Vlad Rusu, Dorel Lucanu. A K-Based Formal Framework for Domain-Specific Modelling Languages. In Bernhard Beckert, Ferruccio Damiani, Dilian Gurov, editors, Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers. Volume 7421 of Lecture Notes in Computer Science, pages 214-231, Springer, 2011. [doi]
We propose a formal approach for the definition of domain-specific modelling languages (DSMLs). The approach uses basic Model-Driven Engineering artifacts for defining a DSML’s syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the K semantic framework. The mapping is implemented in the Rascal metaprogramming language. Since the resulting K definitions are executable, one obtains an execution engine for DSMLs and gains acces to K’s formal analysis tools. We illustrate the approach on xSPEM, a language for describing the execution of tasks constrained by time, precedence, and resources.
Available at http://hal.inria.fr/inria-00637099.