PsyC

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