Design and validation of a C++ code generator from Abstract State Machines specifications

S. Bonfanti, A. Gargantini, A. Mashoor. Design and validation of a C++ code generator from Abstract State Machines specifications. Journal of Software: Evolution and Process, Special Issue: Security- and Safety-Critical Cyber-Physical Systems, volume 32, number 2, pages e2205, DOI 10.1002/smr.2205, 2, 2020.

Autoren
  • Silvia Bonfanti
  • Angelo Gargantini
  • Atif Mashoor
TypArtikel
JournalJournal of Software: Evolution and Process, Special Issue: Security- and Safety-Critical Cyber-Physical Systems
Nummer2
Band32
DOI10.1002/smr.2205
Monat2
Jahr2020
Seitene2205
Abstract

According to best practices of model‐driven engineering, the implementation of a system should be obtained from its model through a systematic model‐to‐code transformation. We present in this paper a methodology supported by the Asm2C++ tool, which allows the users to generate C++ code from abstract state machine models. Thanks to Asm2C++, the implementation is generated in a seamless manner with an assurance of potential bug freeness of the generated code. Following the same approach, model‐based testing suggests deriving also (unit) tests from abstract models. We extend the Asm2C++ tool such that it can automatically produce unit tests for the generated code. Abstract test sequences, either generated randomly or through model checking, are translated to concrete C++ unit tests using the Boost library. In a similar manner, also, scenarios are generated in a behavior‐driven development (BDD) approach. To guarantee the correctness of the transformation process, we define a mechanism to test the correctness of the model‐to‐code transformation with respect to two main criteria: syntactical correctness and semantic correctness, which is based on the definition of conformance between the specification and the code. Using this approach, we have devised a process able to test the generated code by reusing unit tests. The process has been used to validate our model‐to‐code transformations.