promotor: prof.dr. M.G.J. van den Brand (TU/e)
copromotors: dr.ir. T.A.C. Willemse (TU/e) and dr.ir. R.R.H. Schiffelers (ASML and TU/e)
Technische Universiteit Eindhoven
Date: 21 November 2017, 16.00
Domain Specific Languages (DSLs) are a central concept of Model Driven Engineering (MDE). They are considered to be very effective in software development and are being widely adopted by industry nowadays. A DSL is a (small) computer language specialized for a specific (application) domain. In the context of MDE, a DSL is usually implemented as a translation to the input language of a target execution platform, such as C/C++ or Java code. As a consequence, the semantics of the DSL is (hard)coded in model transformations and code generation. This situation poses challenges when designing, learning, and evolving the DSL. In this work we investigated how an explicit definition of the dynamic semantics of a DSL can facilitate design and development of the DSL, and support understanding and debugging of DSL programs.
In order to gain insight into a real-life experience of working on and with DSLs, we performed a case study at ASML, a producer of complex lithography machines for the semiconductor industry. In our case study we defined the dynamic semantics of the LACE DSL (Logical Action Component Environment), which is used for generating fragments of the source code that controls lithography machines. Aiming for practical benefits of having a formal definition of the DSL dynamic semantics, we employed a formalism that has extensive tool support: the Event-B formalism. The Rodin platform offers a wide range of functionality that can be applied to an Event-B specification of the DSL: editing, automatic generation of proof obligations, automatic and interactive proving, animation, model checking, etc. To be able to apply these tools to a DSL specification, we used Event-B as a back-end formalism for defining the dynamic semantics of the DSL and developed a model-to-model transformation from the DSL to Event-B. To engage DSL engineers who are not familiar with the notation of Event-B, we created a domain-specific visualization of the Event-B specifications of the DSL. The visualization mimics the original graphical notation of the DSL and runs on top of the animation of an Event-B specification. Using this visualization, we investigated the needs and the perception of DSL engineers by means of a user study. Based on the lessons learned during the case study and on the results of the user study, we formulated the use cases for a definition of the dynamic semantics of a DSL and identified the corresponding requirements. For example, we have observed that although the available tools facilitate design and usage of the DSL, the semantic gap between the DSL and Event-B is quite wide, and the definition of the dynamic semantics is kept (coded) in the DSL-to-Event-B translation. Thus, the abstraction level of Event-B is not enough for defining the dynamic semantics of DSLs. An example of an important requirement, indicated by the DSL engineers, is that the DSL specification should be (kept) consistent with the actual implementation of the DSL (which evolves over time).
To bridge the wide semantic gap between a DSL and a specification formalism and to facilitate consistency between the specification and the implementation of a DSL, we introduce an intermediate semantic domain, that splits the semantic mapping from a DSL to an execution platform (or a specification formalism) into two steps. As such an intermediate semantic domain we use software design solutions that are typically used in the DSL implementation, i.e. concepts that form the horizontal domain of the DSL. Thus, we propose to define the dynamic semantics of a DSL as a mapping from the language constructs (forming the vertical domain of the DSL) to the horizontal concepts. We realized the proposed idea in the form of the Constelle language and reusable specification templates. Specification templates realize the generic programming paradigm for (thorough mathematical-based) formal specifications. They capture software design solutions of the DSL horizontal domain in the form of generic (Event-B) specifications that can be specialized for a concrete domain. Constelle allows for defining the DSL dynamic semantics as a composition of such specification templates and, in this way, implements the two-step translation of the DSL to the back-end formalism. For invoking and weaving templates, Constelle applies ideas of aspect oriented programming and uses the notation of a table: the DSL vertical domain is represented in the table rows, the DSL horizontal domain is represented in the table columns, and the mapping from the vertical to the horizontal domain is represented in the table intersections.
The semantics of the Constelle language is implemented as a model-to-model transformation from Constelle to Event-B. We describe this transformation informally through the mathematical notation of set theory and functions. While designing the Constelle-to-Event-B transformation, we used this notation to formulate and to apply two design principles of developing (QVTo) model transformations: structural decomposition and chaining model transformations.
To evaluate our approach, we designed and conducted a validation study on defining the dynamic semantics of a DSL using Constelle. The validation study was designed as an action research, following the steps of the GQM (Goal, Question, Metric) method.
The validation study revealed both strong sides and limitations of applying Constelle. Moreover, based on the insights gained during the study we formulated a number of interesting directions for future work.