2013 | OriginalPaper | Buchkapitel
A Mechanized Semantic Framework for Real-Time Systems
verfasst von : Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali-Amine
Erschienen in: Formal Modeling and Analysis of Timed Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 C
oq
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.