Modeling and Verifying Distributed and Real-Time Systems using Timed Automata with Partially Independent Clocks

Abstract

Distributed Real-Time Systems (DRTS) play an increasingly important role in everyday life, from traffic light controllers to airplanes, and from telecommunication networks to medical systems. In the last decades, several formal methods and real-time formalisms have been proposed to formalize and prove properties of DRTS. However, traditional real-time formalisms are not always adequate for reasoning about DRTS because they assume a unique, perfectly synchronous (Newtonian) measure of time. The most successful techniques for modeling real-time systems (RTS) are Timed Automata (TA), Event Clock Automata (ECA), and Recursive Event Clock Automata (RECA). A TA is a finite automaton augmented with real-valued clocks, where all clocks have infinite precision and are perfectly synchronized. There are other variants of TA called Distributed Timed Automata (DTA) and Timed Automata with Independent Clocks (icTA), proposed by Krishnan et al. and Akshay et al. to model DRTS where the clocks are not necessarily synchronized. DTA and icTA are neither determinable nor complementable, and their inclusion problems are undecidable. In this thesis, we remove the above problems of undecidability, perfect clock synchronization, and single timestamps. We introduce three alternative semantics:
(i) Distributed Event Clocks: We propose a formal semantics for modeling DRTS based on Recursive Event Clock Automata (RECA) with such independent clocks, yielding the Distributed Recursive Event Clock Automata (DECA).
(ii) Multiple Independent Clocks: We extend the standard semantics of TA and timed bisimulation to include the notion of multiple independent clocks. Therefore, we extend the semantics of icTA to work with the notion of multi-timed words.
(iii) Distributed Clock Derivatives: We extend the semantics of TA to include the notion of distributed clock derivatives. Therefore, we extend the TA to work with the notion of clock derivatives, yielding the Timed Automata with Clock Derivatives (DMTA).

Date of Award	4 Jul 2023
Original language	English
Awarding Institution	University of Namur
Sponsors	University of Namur
Supervisor	Pierre Yves Schobbens (Supervisor), Jean-Marie Jacquet (Jury), Wim Vanhoof (Jury), Jean-Francois Raskin (Jury), Stavros Tripakis (Jury) & S. Akshay (Jury)