salle A. Turing CE4
26 September 2013 - 14h00
A Mechanized Semantic Framework for Real-Time Systems
by Garnacho Manuel from 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.
