OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

From Lustre to Simulink: reverse compilation for verifying Embedded Systems Applications

Bourbouh, Hamza and Garoche, Pierre-Loïc and Garion, Christophe and Thirioux, Xavier From Lustre to Simulink: reverse compilation for verifying Embedded Systems Applications. (2021) ACM Transactions on Cyber-Physical Systems, 5 (3). 1-20. ISSN 2378-962X

[img] (Document in English)

PDF (Author's version) - Depositor and staff only until 21 December 2021 - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
3MB

Official URL: https://doi.org/10.1145/3461668

Abstract

Model-based design is now unavoidable when building embedded systems and more specifically controllers. Among the available model languages, the synchronous dataflow paradigm, as implemented in languages such as Matlab Simulink or ANSYS Scade, has become predominant in the critical embedded system industries. Both of these frameworks are used to design the controller itself but also provide code generation means, enabling faster deployment to target and easier V\&V activities performed earlier in the design process, at model level. Synchronous models also ease the definition of formal specification through the use of synchronous observers, attaching requirements to the model in the very same language, mastered by engineers and tooled with simulation means or code generation. However, few works address the automatic synthesis of Matlab Simulink annotations from lower level models or code. We present here a compilation process from Lustre models to genuine Matlab Simulink, without the need to rely on external C functions or Matlab functions. This re-engineering is then used to validate a compilation tool-chain, mapping Simulink to Lustre and then C, thanks to equivalence testing and checking. This backward-compilation from Lustre to Simulink also provides the ability to produce automatically Simulink components modeling specification, proof arguments or test cases coverage criteria.

Item Type:Article
HAL Id:hal-03323076
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Ecole Nationale de l'Aviation Civile - ENAC (FRANCE)
Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > National Aeronautics and Space Administration - NASA (USA)
Laboratory name:
Statistics:download
Deposited On:20 Aug 2021 09:38

Repository Staff Only: item control page