AbstractIn this paper, we present Clock Difference Diagrams (CDD), a new BDD-like data-structure for effective representation and manipulation of certain non-convex subsets of the Euclidean space, notably those encountered in verification of timed automata. It is shown that all set-theoretic operations including inclusion checking may be carried out efficiently on Clock Difference Diagrams. Other clock operations needed for fully symbolic analysis of timed automata e.g. future- and reset-operations, can be obtained based on a so-called tight normalform for CDD. A version of the real-time verification tool UPPAAL using Clock Difference Diagrams as the main data-structure has been implemented. Experimental results demonstrate significant space-savings: for nine industrial examples the savings are in average 42% with moderate increase in runtime.
Categories and Subject Descriptors: D.2.1 [Software Engineering]: Requirements/Specifications; D.2.2 [Software Engineering]: Tools and Techniques; D.2.4 [Software Engineering]: Program Verification; I.2.2 [Artificial Intelligence]: Automatic Programming; I.6.4 [Simulation and Modeling]: Model Validation and Analysis; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs
Additional Key Words and Phrases: automatic verification, real-time systems, timed automata, symbolic model-checking, clock difference diagrams
Selected references
- Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Michael S. Paterson, editor, Automata, Languages and Programming, 17th International Colloquium, volume 443 of Lecture Notes in Computer Science, pages 322-335, Warwick University, England, 16-20 July 1990. Springer-Verlag.
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: $10^{20}$ states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428-439, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994.
- Carsten Weise and Dirk Lenzkes. Efficient scaling-invariant checking of timed bisimulation. In 14th Annual Symposium on Theoretical Aspects of Computer Science, volume 1200 of Lecture Notes in Computer Science, pages 177-188, Lübeck, Germany, 27 February-mar 1 1997. Springer.