Analysis of timed systems using time-abstracting bisimulations.

*(English)*Zbl 0971.68096Summary: The objective of this paper is to show how verification of dense-time systems modeled as timed automata can be effectively performed using untimed verification techniques. In that way, the existing rich infrastructure in algorithms and tools for the verification of untimed systems cn be exploited. The paper completes the ideas introduced in S. Tripakis and S. Yovine [Proc. 8th Conf. Computer-Aided Verification, CAV ’96, Rutgers, NJ (1996), Lect. Notes Comput. Sci. 1102, 232-243 (1996)].

Our approach consists in two steps. First, given a timed system \(A\), we compute a finite graph \(G\) which captures the behavior of \(A\) modulo the fact that exact time delays are abstracted away. Then, we apply untimed verification techniques on \(G\) to prove properties on \(A\). As property-specification languages, we use both the linear-time formalism of Timed Büchi Automata (TBA) and the branching-time logic TCTL. Model checking \(A\) against properties specified as TBA or TCTL formulae comes down to applying, respectively, automata-emptiness or CTL model-checking algorithms on \(G\).

The abstraction of exact delays is formalized under the concept of time-abstracting bisimulations. We define three time-abstracting bisimulations which are strictly ordered with respect to their reduction power. The stronger of them preserves both linear- and branching-time properties whereas the two weaker ones preserve only linear-time properties.

The finite graph \(G\) is the quotient \(A\) with respect to a time-abstracting bisimulation. Generating \(G\) is called minimization and can be done by adapting a partition-refinement algorithm to the timed case. The adapted algorithm is symbolic, that is, equivalence classes are represented as simple polyhedra. When these polyhedra are not convex, operations become expensive, therefore, we develop a partition-refinement technique which preserves convexity.

We have implemented the minimization algorithm in a prototype module called minim, as part of the real-time verification platform KRONOS minim connects KRONOS to the CADP tool suite for the verification of untimed graphs [J. Cl. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriquez and J. Sifakis, A tool box for the verification of lotos programs, 14th International Conference on Software Engineering (1992)]. To demonstrate the practical interest behind our approach, we present two case studies, namely, Fisher’s mutual exclusion protocol and the CSMA/CD communication protocol.

Our approach consists in two steps. First, given a timed system \(A\), we compute a finite graph \(G\) which captures the behavior of \(A\) modulo the fact that exact time delays are abstracted away. Then, we apply untimed verification techniques on \(G\) to prove properties on \(A\). As property-specification languages, we use both the linear-time formalism of Timed Büchi Automata (TBA) and the branching-time logic TCTL. Model checking \(A\) against properties specified as TBA or TCTL formulae comes down to applying, respectively, automata-emptiness or CTL model-checking algorithms on \(G\).

The abstraction of exact delays is formalized under the concept of time-abstracting bisimulations. We define three time-abstracting bisimulations which are strictly ordered with respect to their reduction power. The stronger of them preserves both linear- and branching-time properties whereas the two weaker ones preserve only linear-time properties.

The finite graph \(G\) is the quotient \(A\) with respect to a time-abstracting bisimulation. Generating \(G\) is called minimization and can be done by adapting a partition-refinement algorithm to the timed case. The adapted algorithm is symbolic, that is, equivalence classes are represented as simple polyhedra. When these polyhedra are not convex, operations become expensive, therefore, we develop a partition-refinement technique which preserves convexity.

We have implemented the minimization algorithm in a prototype module called minim, as part of the real-time verification platform KRONOS minim connects KRONOS to the CADP tool suite for the verification of untimed graphs [J. Cl. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriquez and J. Sifakis, A tool box for the verification of lotos programs, 14th International Conference on Software Engineering (1992)]. To demonstrate the practical interest behind our approach, we present two case studies, namely, Fisher’s mutual exclusion protocol and the CSMA/CD communication protocol.

##### MSC:

68Q45 | Formal languages and automata |