Publications

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
Static Analysis of Contextual Memory Accesses for Safe Memory Sharing
Static analysis of contextual memory accesses in real-time kernels to help enforce safe memory-sharing policies between kernel and application components.
Florent Sagot, Jean Guyomarc'h, Fabien Siron
Source Document
Separation of Functional and Time Interference Concerns for Efficient AMC 20-193 Compliance
A time-aware design approach based on synchronous Logical Execution Time for separating functional and timing interference concerns in multicore avionics systems.
Damien Chabrol, Jean Guyomarc'h, Fabien Siron, Guillaume Phavorin, Sam Thompson, Eric Jenn, François Thurieau
PDF Source Document
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
Vérification d'applications temps-réel basées sur le paradigme de Logical Execution Time (LET)
French doctoral-session paper on adapting verification techniques from synchronous languages to real-time applications based on Logical Execution Time.
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