Publication
Title
Towards domain-specific property languages : the ProMoBox approach
Author
Abstract
Domain-specific modeling (DSM) is one major building block of model-driven engineering. By moving from the solution space to the problem space, systems are designed by domain experts. The benefits of DSM are not unique to the design of systems, the specification and verification of desired properties of the designed systems by the help of DSM seems the next logical step. However, this latter aspect is often neglected by DSM approaches or only supported by translating design models to formal representations on which temporal properties are defined and evaluated. Obviously, this transition to the solution space is in contradiction with DSM. To shift the specification and verification tasks to the DSM level, we extend traditional Domain-Specific Modeling Languages (DSMLs) for design with ProMoBox, a language family comprising three DSMLs covering design, property specification, and verification results. By using ProMoBox, temporal properties can be described for finite-state systems and verified by the SPIN model checker, by compiling them to Promela and Linear Temporal Logic (LTL). For specifying properties we present a DSML that is based on Dwyer's specification patterns and mash it up with adapted versions of the design DSML to formulate structural patterns. In particular, we show that a ProMoBox can be generated from a single root meta-model and we demonstrate our approach with a ProMoBox for statecharts.
Language
English
Source (book)
Proceedings of the 2013 ACM Workshop on Domain-Specific Modeling
Publication
New York, N.Y. : ACM, 2013
ISBN
978-1-4503-2600-1
Volume/pages
p. 39-44
Full text (Publisher's DOI)
UAntwerpen
Faculty/Department
Research group
Publication type
Subject
Affiliation
Publications with a UAntwerp address
External links
Record
Identification
Creation 13.02.2014
Last edited 22.11.2016
To cite this reference