Real-time Extensions for the Fiacre modeling language
Résumé
We present our ongoing research on the extension of the Fiacre language with real-time constructs and real-time verification patterns. Fiacre is a formal language with support for expressing concurrency and timing constraints; its goal is to act as an intermediate format for the formal verification of high-level modeling language, such as Architecture Description Languages or UML profiles for system modeling. Essentially, Fiacre is designed both as the target of model transformation engines from various languages, as well as the source language of compilers into verification toolboxes, namely Tina and CADP. Our motivations for extending Fiacre are to reduce the semantic gap between Fiacre and high-level description languages and to streamline our verification process.