Automatic code generation from formal specification: UASM to C++ for Arduino

• Marco Carissoni

Formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, it is possible to verify the system’s properties in a more thorough fashion than empirical testing.

The ASM method [2] is a mathematical formalism used in software engineering during requirements elicitation phase. Its purpose is to bridge the gap between the human formulation of a real-world problem and the corresponding algorithmic solution. UASM (Unified ASM language) [3] is the common notation born from the need of the two main ASM communities to have a unique syntax.

Formal methods gain their value in safety-critical systems because they provide a means to assure correctness and consistency of the model. There are many successful stories in applying formal methods to real-world problems. One example is Meteor, the driver-less line 14 metro in Paris [4].

Although formal methods seem to be very promising, they are generally viewed with suspicion by the professional engineering community. In fact, because of the rigor involved, formal methods are seem to be more expensive than traditional approaches to engineering [5]. Industrial authors have expressed frustration in trying to incorporate formal technologies into practical software development for many reasons: the perception that they add lengthy stages to the process; they require extensive personnel training; or they are incompatible with other software packages [6].

The aim of this thesis is to realize a translation scheme from UASM specifications to C++ for Arduino. The goal is to boost the integration of the ASM method within a model-driven development process. In particular the project consists of building a code generation tool that from the UASM specification automatically produces the corresponding C++ code for Arduino.