Formal verification of real-time safety-critical systems: application to the PsyC language

Fabien Siron le 12/6/2024, 1:00:00 PM

Lieu: Salle 1073

Important note

The seminar will be held at Nano-Innov only. There will not be a Livestorm retransmission.

Abstract

Safety-critical real-time systems have to respect strict timing constraints. Thus, timing constraints must be considered throughout the software development cycle. As exact computation execution time are generally not known during design, logical time provides a way to abstract time constraints and execution from platform-dependent physical time. In this thesis, we focus on two main formalisms based on logical time:

The Synchronous-Reactive approach totally abstracts physical time by discrete time bases on which computations are triggered.
The Logical Execution Time approach uses logical time bases to represent not only triggering instants but also the durations of elementary computations. We start by unifying Synchronous-Reactive and Logical Execution Time approaches. This provides the natural formal framework for defining the semantics of PsyC, an expressive industrial real-time language. We define two formal semantics for PsyC:
1. a native big-step semantics preserving the logical durations of time intervals defined by structural operational rules and;
2. a synchronous small-step semantics defined by translation to a Synchronous-Reactive language expanding time interval durations to a succession of atomic transitions. We show that the two semantics definitions are equivalent. This formalization of the PsyC semantics enables us to define a formal verification methodology for PsyC based on symbolic model-checking. To reduce the state space during model-checking, we also define an optimization technique inspired by timed automata model-checking. Finally, we show how to encode high-level timing requirements into a clock constraint specification language — CCSL — which are then translated to synchronous observers.