OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Mechanized Semantic Framework for Real-Time Systems

Garnacho, Manuel and Bodeveix, Jean-Paul and Filali, Mamoun A Mechanized Semantic Framework for Real-Time Systems. (2013) In: 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2013), 29 August 2013 - 31 August 2013 (Buenos Aires, Argentina).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/978-3-642-40229-6_8


Concurrent systems consist of many components which may execute in parallel and are complex to design, to analyze, to verify, and to implement. The complexity increases if the systems have real-time constraints, which are very useful in avionic, spatial and other kind of embedded applications. In this paper we present a logical framework for defining and validating real-time formalisms as well as reasoning methods over them. For this purpose, we have implemented in the Coq proof assistant well known semantic domains for real-time systems based on labelled transitions systems and timed runs. We experiment our framework by considering the real-time CSP-based language fiacre, which has been defined as a pivot formalism for modeling languages (aadl, sdl, ...) used in the TOPCASED project. Thus, we define an extension to the formal semantic models mentioned above that facilitates the modeling of fine-grained time constraints of fiacre. Finally, we implement this extension in our framework and provide a proof method environment to deal with real-time system in order to achieve their formal certification.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 8053 Lecture Notes in Computer Science ISSN : 0302-9743. ISBN: 978-3-3xx. The original PDF is available at :
HAL Id:hal-01231769
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:28 Oct 2015 13:10

Repository Staff Only: item control page