Recent work in the group falls into the following themes.
Analysis of models
Just like code, models need to be checked for correctness. Moreover, models are often created to facilitate some kind of analysis. Our recent work has focused on the development and implementation of analyses of executable models to facilitate, e.g., the debugging and testing models, the generation of test cases from models, and the argument that the model satisfies certain properties. To support these analyses, we have done work allowing the animation (using, e.g., the Unity game and virtual reality development platform, unity3d.com), monitoring, tracing and steering of model executions, but we have also helped define the semantics of modeling languages formally.
Most of this work has been carried out in the context of notations such as UML, UML-RT, or AADL and tools such as Papyrus-RT (eclipse.org/papyrus-rt), IBM RoseRT, IBM RSA-RTE, IBM Rhapsody, and OSATE.
Transformation and evolution of models
Apart from analysis, many activities on models involve some kind of transformation or evolution. Recent work in the group has aimed at facilitating the authoring of correct transformations and migrations, reconciling evolution and analysis by making analyses incremental and allowing them to leverage previous analysis results, and identifying techniques and tools for reasoning about the preservation of the semantics of a model that has undergone some change.
Supporting technology used for this work includes ATL, Alloy, Klee, OWL, Sparql, DSLTrans, IBM Rhapsody, and Sodius MDWorkbench.
Formal specification and verification
Certain kinds of analyses allow the formal verification of the model with respect certain properties. Such analyses are typically based on some kind of exhaustive state space exploration (a.k.a., model checking) or the use of symbolic representations (often in terms of logical formulas) of the semantics of the model. Areas of application include domains with safety-critical software as found, for instance, in automobiles.
Tools we have used for this kind of work include Spin, Java Pathfinder, NuSMV, Choco, and UppAal.
Synthesis and correctness by construction
With the help of our background in formal specification and analysis, we have developed techniques for the automatic generation of software that is correct-by-construction and that, therefore, does not need to be tested or verified. Areas of application include concurrent software, web service composition, and dynamic scheduling and reconfiguration for fault-tolerance.
Most of this work uses results and tools from Discrete Event Control Theory and timed automata.
Demonstrators for model-based development
To illustrate the use model-based software development for embedded, reactive systems and evaluate our ideas and prototypes, we have been using a rover, i.e., a small, low-cost vehicle inspired by the Eclipse PolarSys Rover (www.polarsys.org/projects/polarsys.rover).
Surveys, comparisons, literature reviews
For many fields and areas of research, it is surprisingly hard to determine the true state-of-the-art. Comparisons, surveys, and literature reviews can be extremely valuable in this sense and we have created a range of them on topics including model transformation tools, model-driven engineering tools, model transformation testing, timed automata, software evolution, and specification languages for dynamic software architectures.