Research area: engineering of modelling languages, metamodelling, requirements modelling, requirements
verification, model transformation
 
We want to be able to *use* domain-specific languages (DSLs). We do not just model systems for the beauty
of it, it is a means to reason about the system on the right level of abstraction. Reasoning involves the
critical but too often neglected tasks of requirements verification, analysis and simulation. These three
tasks are performed to check precisely defined properties in a model. To achieve these tasks, we typically
benefit on the one hand from precisely defined formalisms such as Petri nets, DEVS, Automata, etc. by
defining a semantic mapping of our DSL onto one of these formalisms.
On the other hand, we describe our properties in a precisely described language as well, such as
e.g., CTL. By using models in such generally known which come with theories, techniques and tools,
we can perform verification, analysis and simulation (verifying syntactic (structural and value) OCL
constraints on an UML model, checking CTL properties on a Büchi Automaton, checking for patterns in an
execution trace, etc.).
 
Two of the main reasons for using DSLs are that they are at the right level of abstraction for their
particular domain, therefore capturing only the essential complexity of the problem, and that they are
very understandable by domain experts, if possible even to the point that they can use them without a
background in computer science. The most pertinent examples are found in domains where the "semantic
domain" is not, and cannot be, software. In biological domains for example, the semantic domain
is often Differential Algebraic Equations. Both reasons suggest that a DSL-user of a DSL should
only have contact with this DSL-layer. Nowadays however, the user still has to define properties in
languages such as CTL. These property languages are not domain-specific.

At Bellairs, I would like to investigate how we can systematically create property languages that *are*
domain-specific. To go even a step further, my goal is to automatically generate property languages
(abstract syntax, concrete syntax and semantic mapping) for a DSL – the Property DSL – given (a) the DSL
metamodel (abstract syntax definition – in our case this is based on class diagrams), (b) the DSL’s
concrete syntax definition (in our case a visual, topologic syntax), (c) the semantic domain of the DSL (a
well-known language such as Petri nets, DEVS, Automata, etc.) and (d) the class of properties the user
wants to verify (from a tentative classification including the class of structural properties, the class
of temporal properties, …). The process of generating a Property DSL is then as follows. The user
parameterizes the Property DSL by choosing a class of properties that can be checked on the semantic
domain (e.g., temporal properties can be checked as CTL-formulas on Büchi Automata, or structural
properties can be checked as OCL-constraints on UML models). This way, the semantic domain of the Property
DSL is chosen (e.g., CTL or OCL). Then, the metamodel of this semantic domain is adapted in such a way
that it refers to the concepts of the DSL, and such that the language is maximally restricted in
accordance with the DSL. In the case of a textual semantic domain such as CTL or OCL, a visual flavour can
be added (such as e.g., TimeLine as a visual flavour for LTL). I believe that with the right toolkit, this
can be done automatically.
The properties defined in the Property DSL can be verified by translating the
properties and the model of the system to models in their respective semantic domains and perform the
check at that level. Notice that results must be returned, which can possibly in the form of execution
traces. They also should be presented at a domain-specific level, so a Traces DSL (analogue to the
Property DSL) might also be desirable. In case of simulation, an Input DSL might be desirable.
The generation of traceability links will of course be crucial.
 
Florian Klein and Holger Giese did some tremendous work on how to re-use a language definition in order to
allow checking properties on abstract syntax graphs. Interestingly, they present a concrete syntax that is
very similar to the concrete syntax for modelling. This is a must-read when joining the little topic/group
proposed.
As an example of how a visual syntax can be created for temporal properties, you should read the work at
Bell labs by Smith et al.
http://msdl.cs.mcgill.ca/conferences/CAMPaM/2012/repository/material/papers/Klein-Giese-TR-RI-06-277.pdf
http://msdl.cs.mcgill.ca/conferences/CAMPaM/2012/repository/material/papers/smith_holzmann_etessami.pdf
 
This research is in the context of modular design of domain-specific languages. I believe that a DSL and
its Property DSL are inseparable. Together they form a "ProMoBox", encapsulating a Properties and a design
Model. After all, what is the purpose of a model without explicit definition of
its use, in our case in the form of properties. In my research I also intend to examine how languages and
their property languages can be combined to form new languages. This should be investigated at a syntactic
level (how to weave languages and their instances) and at the level of its semantics. With respect to the
latter, Joachim and I worked on a hybrid language which combines state-charts (discrete time) and
causal block diagrams (continuous time). We intend to explicitly model the interface between both 
simulators and generalise these interface concepts. There is an obvious link with the work on 
ModHel'X and similar multi-formalism simulation frameworks.