Parameterized Model-Checking for Timed-Systems with Conjunctive Guards (Extended Version)

TL;DR

This paper extends cutoff theorems to parameterized networks of timed automata with conjunctive guards, enabling verification of systems with unknown numbers of heterogeneous timed processes, including protocols using process identifiers.

Contribution

It generalizes existing cutoff results to timed automata with conjunctive guards and PIDs, facilitating the verification of complex, parameterized real-time distributed systems.

Findings

Extended cutoff theorems to timed automata with conjunctive guards

Modeled and verified protocols using process identifiers in timed automata

Provided a framework for verifying heterogeneous, parameterized timed systems

Abstract

In this work we extend the Emerson and Kahlon's cutoff theorems for process skeletons with conjunctive guards to Parameterized Networks of Timed Automata, i.e. systems obtained by an \emph{apriori} unknown number of Timed Automata instantiated from a finite set $U_1, \dots, U_n$ of Timed Automata templates. In this way we aim at giving a tool to universally verify software systems where an unknown number of software components (i.e. processes) interact with continuous time temporal constraints. It is often the case, indeed, that distributed algorithms show an heterogeneous nature, combining dynamic aspects with real-time aspects. In the paper we will also show how to model check a protocol that uses special variables storing identifiers of the participating processes (i.e. PIDs) in Timed Automata with conjunctive guards. This is non-trivial, since solutions to the parameterized verification problem often relies on the processes to be symmetric, i.e. indistinguishable. On the other side, many popular distributed algorithms make use of PIDs and thus cannot directly apply those solutions.