↓Skip to main content

Real-time Extensions for the Fiacre modeling language

Verification Architecture Languages Fiacre
Table of Contents

Nouha Abid, Silvano Dal Zilio
preprint, jun 2010.

unpublished

 PDF  HAL-00494617

Note
#

presentation at MoVep 2010 — summer school on Modelling and Verifying Parallel Processes

Abstract
#

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.

Citation
#


@Unpublished{DalzilioS:movep2010,
   author      = {Abid, Nouha and {Dal Zilio}, Silvano},
   title       = {{Real-time Extensions for the Fiacre modeling language}},
   month       = jun, 
   year        = 2010
}