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 con- structs 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 verifica- tion 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 en- gines 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.
Domaines
Théorie et langage formel [cs.FL]
Fichier principal
Abid_Nouha_LAAS.pdf (51.5 Ko)
Télécharger le fichier
class.pdf (78.41 Ko)
Télécharger le fichier
Origine : Accord explicite pour ce dépôt
Format : Autre
Loading...