Skip to main content
SpringerLink
Log in

Verification Support for a State-Transition-DSL Defined with Xtext

  • Conference paper
  • First Online:
Book cover Perspectives of System Informatics (PSI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9609))

Abstract

A Domain-Specific Language (DSL) allows the succinct modeling of phenomena in a problem domain. Modern DSL-tools make it easy for a language designer to define the syntax of a new DSL, to specify code generators or to build a new DSL on top of existing DSLs. Based on the language specification, the DSL-tool then generates rich editors. Often, these editors support features such as syntax highlighting, code completion or automatic refactoring.

In this paper, we describe an approach of adding verification support for DSLs defined within the Eclipse-framework Xtext. Xtext provides good support for checking the well-formedness rules of the DSL’s syntax. In contrast, support for specifying the language’s semantics as well as verification support have been rather neglected so far. Our approach of incorporating semantic verification techniques is illustrated by a very simple State-Transition-DSL, which has been fully implemented in Xtext. The DSL’s editor verifies on the fly that the current model holds some semantic properties such as deterministic execution and invariant preservation. The verification services for this DSL are based on the theorem prover Princess.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Due to the paper’s page limit, only the important parts of the grammar are presented here. The full grammar is available from [5].

References

  1. Aßmann, U., Bartho, A., Bürger, C., Cech, S., Demuth, B., Heidenreich, F., Johannes, J., Karol, S., Polowinski, J., Reimann, J., Schroeter, J., Seifert, M., Thiele, M., Wende, C., Wilke, C.: Dropsbox: the Dresden open software toolbox - domain-specific modelling tools beyond metamodels and transformations. Softw. Syst. Model. 13(1), 133–169 (2014)

    Article  Google Scholar 

  2. Yakindu: Homepage. http://statecharts.org/

  3. Xtext: Homepage. http://www.eclipse.org/Xtext/

  4. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  5. Baar, T.: SSMA - Simple State Machine Analyzer. https://github.com/thomasbaar/simplesma

  6. Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing, Birmingham (2013)

    Google Scholar 

  7. Ghezzi, C., Menghi, C., Sharifloo, A.M., Spoletini, P.: On requirement verification for evolving statecharts specifications. Requir. Eng. 19(3), 231–255 (2014)

    Article  Google Scholar 

  8. Prashanth, C.M., Shet, K.C.: Efficient algorithms for verification of UML statechart models. JSW 4(3), 175–182 (2009)

    Article  Google Scholar 

  9. Rümmer, P.: Princess homepage. http://www.philipp.ruemmer.org/princess.shtml

  10. Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Bettini, L.: Xsemantics Documentation (2015). http://xsemantics.sourceforge.net/documentation/

  12. Wachsmuth, G., Konat, G.D.P., Visser, E.: Language design with the Spoofax language workbench. IEEE Softw. 31(5), 35–43 (2014)

    Article  Google Scholar 

  13. Vergu, V.A., Neron, P., Visser, E.: Dynsem: a DSL for dynamic semantics specification. In: Fernández, M., (ed.) 26th International Conference on Rewriting Techniques and Applications, RTA 29 to 1 July 2015, Warsaw, Poland, vol. 36 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 365–378, June 2015

    Google Scholar 

  14. Object Management Group: Unified Modeling Language (UML), version 2.5, June 2015. http://www.omg.org/spec/UML/2.5/

Download references

Author information

Authors and Affiliations

  1. Hochschule für Technik und Wirtschaft (HTW) Berlin, Wilhelminenhofstraße 75A, 12459, Berlin, Germany

    Thomas Baar

Authors
  1. Thomas Baar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thomas Baar .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Baar, T. (2016). Verification Support for a State-Transition-DSL Defined with Xtext. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41579-6_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41578-9

  • Online ISBN: 978-3-319-41579-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation