Abstract
In this paper we address the problem of distributing model checking of timed automata. We demonstrate through four real life examples that the combined processing and memory resources of multi-processor computers can be effectively utilized. The approach assumes a distributed memory model and is applied to both a network of workstations and a symmetric multiprocessor machine. However, certain unexpected phenomena have to be taken into account. We show how in the timed case the search order of the state space is crucial for the effectiveness and scalability of the exploration. An effective heuristic to counter the effect of the search order is provided. Some of the results open up for improvements in the single processor case.
Research supported by Esprit Project 26270, Verification of Hybrid Systems (VHS).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aggarwal, S., Alonso, R., Courcoubetis, C.: Distributed reachability analysis for protocol verification environments. In: Discrete Event Systems: Models and Applications. IIASA Conference, pp. 40–56 (1987)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Caselli, S., Conte, G., Marenzoni, P.: Parallel state space exploration for GSPN models. In: DeMichelis, G., Díaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 181–200. Springer, Heidelberg (1995)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dill, D.L.: The murϕ verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Havelund, K., Larsen, K., Skou, A.: Formal verification of a power controller using the real-time model checker Uppaal. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 277–298. Springer, Heidelberg (1999)
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio/video protocol: An industrial case study using Uppaal. In: Proc. of the 18th IEEE Real-Time Systems Symposium, San Francisco, California, USA, pp. 2–13 (December 1997)
Haverkort, B.R., Bell, A., Bohnenkamp, H.C.: On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models (PNPM 1999), Zaragoza, Spain, pp. 12–21. IEEE Computer Society Press, Los Alamitos (1999)
Hune, T., Larsen, K.G., Pettersson, P.: Guided synthesis of control programs using Uppaal. In: Proc. of the International Workshop on Distributed Systems, Verification and Validation, Taipei, Taiwan (April 2000)
Kristoffersen, K.J., Laroussinie, F., Larsen, K.G., Pettersson, P., Yi, W.: A compositional proof of a real-time mutual exclusion protocol. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 565–579. Springer, Heidelberg (1997)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Larsson, F., Larsen, K.G., Pettersson, P., Yi, W.: Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)
Lönn, H., Pettersson, P.: Formal verification of a TDMA protocol startup mechanism. In: Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, December 1997, pp. 235–242 (1997)
Snir, M., Otto, S.W., Huss-Lederman, S., Walker, D., Dongarra, J.J.: MPI: The Complete Reference. MIT Press, Cambridge (1996)
Stern, U., Dill, D.L.: Parallelizing the Murϕ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 22–25. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Behrmann, G., Hune, T., Vaandrager, F. (2000). Distributing Timed Model Checking — How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_19
Download citation
DOI: https://doi.org/10.1007/10722167_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive