Synchronous-Reactive Systems

Modular Extraction of Lustre Models from C Reactive Programs using Frama-C
Extraction of synchronous Lustre models from reactive C programs by combining symbolic program analysis and abstract interpretation in Frama-C.
Loïc Correnson, Fabien Siron, Christophe Junke
Project Source Document DOI
Methodology for the Formal Verification of Temporal Properties for Real-Time Safety-Critical Applications Based on Logical Time
PhD thesis on semantic foundations and formal verification of logical-time real-time programs, with applications to PsyC, synchronous languages, symbolic model checking, and CCSL.
Fabien Siron
PDF Slides Source Document
Semantics Foundations of PsyC Based on Synchronous Logical Execution Time
Semantic foundations for the industrial PsyC language based on Synchronous Logical Execution Time, relating LET-style execution to synchronous-reactive semantics.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document DOI
Formal Semantics of the PsyC Language
A formal semantic account of the PsyC real-time language, including its logical-time execution model and its relation to synchronous representations.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document
The Synchronous Logical Execution Time Paradigm
Introduction of synchronous Logical Execution Time (sLET), combining logical durations from LET with multiform logical clocks from synchronous-reactive systems.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document
Programming and Verifying Real-Time Design Using Logical Time
Early work comparing synchronous languages, Logical Execution Time, and PsyC with the objective of reusing synchronous verification techniques for LET-based real-time programs.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document