Verimag

Détails sur le séminaire

salle A. Turing CE4
26 septembre 2013 - 14h00
A Mechanized Semantic Framework for Real-Time Systems
par Garnacho Manuel de IRIT



Abstract: In this talk I will present a logical framework for defining and validating real-time formalisms as well as reasoning methods over them. For this purpose, at first we have implemented in the Coq proof assistant well known semantic domains for real-time systems based on 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 high-level languages (aadl, sdl, ...) used in the TOPCASED project. Thus, we define an extension to the formal semantic models mentioned above that facilitates the formalization of fi ne-grained time constraints of FIACRE.
Finally, we implement this extension in our framework and provide a sound proof-method that enables us to deal with real-time systems in order to achieve their formal certification within COQ.





Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876967