Methodology for the Formal Verification of Temporal Properties for Real-Time Safety-Critical Applications Based on Logical Time

Abstract

The thesis studies formal verification of safety-critical real-time applications whose behavior is expressed using logical time. It develops the Synchronous Logical Execution Time framework connecting Synchronous-Reactive and Logical Execution Time approaches, defines two equivalent semantic descriptions of the PsyC language, and builds a verification methodology based on translation to synchronous models and symbolic model checking. Additional contributions include temporal state-space reduction techniques and the expression of timing requirements using CCSL and synchronous observers.

Fabien Siron

Research Engineer | Lecturer

Research engineer working on formal verification, synchronous-reactive systems and safety-critical real-time software.