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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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
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)
Yakindu: Homepage. http://statecharts.org/
Xtext: Homepage. http://www.eclipse.org/Xtext/
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Baar, T.: SSMA - Simple State Machine Analyzer. https://github.com/thomasbaar/simplesma
Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing, Birmingham (2013)
Ghezzi, C., Menghi, C., Sharifloo, A.M., Spoletini, P.: On requirement verification for evolving statecharts specifications. Requir. Eng. 19(3), 231–255 (2014)
Prashanth, C.M., Shet, K.C.: Efficient algorithms for verification of UML statechart models. JSW 4(3), 175–182 (2009)
Rümmer, P.: Princess homepage. http://www.philipp.ruemmer.org/princess.shtml
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)
Bettini, L.: Xsemantics Documentation (2015). http://xsemantics.sourceforge.net/documentation/
Wachsmuth, G., Konat, G.D.P., Visser, E.: Language design with the Spoofax language workbench. IEEE Softw. 31(5), 35–43 (2014)
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
Object Management Group: Unified Modeling Language (UML), version 2.5, June 2015. http://www.omg.org/spec/UML/2.5/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)