Distributed reachability analysis in timed automata

Gerd Behrmann1
1Department of Computer Science, Aalborg University, Denmark

Tóm tắt

We evaluate a distributed reachability algorithm suitable for verification of real time critical systems modeled as timed automata. It is discovered that the algorithm suffers from load balancing problems and a high communication overhead. The load balancing problems are caused by the symbolic nature of the representation of the states of a timed automaton. We propose alternative data structures for representing the state-space of a timed automaton and adding a proportional load balancing controller on top of the algorithm. We evaluate various approaches at reducing communication overhead by increasing locality and compressing states. It is experimentally evaluated that by using the techniques speedups between 50% and 90% of linear can be obtained on a 14 node Linux Beowulf cluster on medium sized examples.

Tài liệu tham khảo

Allmaier S, Dalibor S, Kreische D (1997) Parallel graph generation algorithms for shared and distributed memory machines. In: Proceedings of the international conference on parallel computing: fundamentals, applications and new directions (ParCo’97), Bonn, Germany, 16–19 September 1997, vol 12, Elsevier, Amsterdam Alur R, Dill DL (1994) A theory of timed automata. Theor Comp Sci 126:183–235 Amnell T, Behrmann G, Bengtsson J, D’Argenio PD, David A, Fehnker A, Hune TS, Jeannet B, Larsen K, Möller O, Pettersson P, Weise C, Yi W (2000) Uppaal – now, next, and future. In: Modeling and verification of parallel processes, 4th summer school (MOVEP 2000), Nantes, France, 19–23 June 2000. Lecture notes in computer science, vol 2067, Springer, Berlin Heidelberg New York Behrmann G (2002) A performance study of distributed timed automata reachability analysis. In: Brim L, Grumberg O (eds) Electronic notes in theoretical computer science, vol 68, Elsevier, Amsterdam Behrmann G, Bouyer P, Fleury E, Larsen KG (2003) Static guard analysis in timed automata verification. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS03), Warsaw, Poland, 7–11 April 2003. Lecture notes in computer science, vol 2619, Springer, Berlin Heidelberg New York Behrmann G, Hune T, Vaandrager F (2000) Distributed timed model checking – how the search order matters. In: Proceedings of the 12th international conference on computer aided verification, Chicago, July 2000. Lecture notes in computer science, vol 1855, Springer, Berlin Heidelberg New York Ben-David S, Heyman T, Grumberg O, Schuster A (2000) Scalable distributed on-the-fly symbolic model checking. In: Proceedings of the 3rd international conference on formal methods in computer aided design (FMCAD’00), Austin, TX, November 2000 Bengtsson J (2001) Reducing memory usage in symbolic state-space exploration for timed systems. Technical Report 2001-009, Uppsala University, Department of Information Technology, Uppsala, Sweden Braberman AOV, Schapachnik F (2002) Zeus: A distributed timed model-checker based on kronos. In: Brim L, Grumberg O (eds) Electronic notes in theoretical computer science, vol 68, Elsevier, Amsterdam Caselli S, Conte G, Marenzoni P (1995) Parallel state space exploration for gspn models. In: Application and theory of Petri nets, Lecture notes in computer science, vol 935, Springer, Berlin Heidelberg New York Ciardo G, Gluckman J, Nicol D (1998) Distributed state space generation of discrete state stochastic models. INFORMS J Comput 10(1):82–93 David A, Behrmann G, Larsen KG, Yi W (2003) Unification & Sharing in Timed Automata Verification. In: Proceedings of the 10th international SPIN workshop on model checking of software (SPIN 2003), Portland, OR, 9–10 May 2003. Lecture notes in computer science, vol 2648 Springer, Berlin Heidelberg New York Dijkstra EW, Scholten CS (1980) Termination detection for diffusing computations. Inform Process Lett 11(1):1–4 Grumberg O, Heyman T, Schuster A (2001) Distributed model checking for mu-calculus. In: Proceedings of the international conference on computer aided verification (CAV’01), Paris, July 2001. Lecture notes in computer science, vol 2102 Springer, Berlin Heidelberg New York Havelund K, Larsen K, Skou A (1999) Formal verification of a power controller using the real-time model checker Uppaal. In: Katoen JP (ed) Proceedings of the 5th international AMAST workshop on formal methods for real-time and probabilistic systems (ARTS’99), Bamberg, Germany, 26–28 May 1999. Lecture notes in computer science, vol 1601, Springer, Berlin Heidelberg New York, pp 277–298 Havelund K, Skou A, Larsen KG, Lund K (1997) Formal modelling and analysis of an audio/video protocol: an industrial case study using Uppaal. In: Proceedings of the 18th IEEE real-time systems symposium. San Francisco, December 1997, pp 2–13 Haverkort BR, Bell A, Bohnenkamp HC (1999) On the efficient sequential and distributed generation of very large markov chains from stochasstic Petri nets. In: Proceedings of the 8th international workshop on Petri nets and performance models PNPM’99, Zaragoza, Spain, 6–10 September 1999. IEEE Press, New York Knottenbelt WJ, Harrison PG (1999) Distributed disk-based solution techniques for large Markov models. In: Proceedings of the 3rd international meeting on the numerical solution of Markov chains (NSMC’99), University of Zaragoza, Spain, September 1999 Larsson F, Larsen KG, Pettersson P, Yi W (1997) Efficient verification of real-time systems: compact data structures and state-space reduction. In: Proceedings of the 18th IEEE real-time systems symposium, San Francisco, 3–5 December 1997. IEEE Press, New York, pp 14–24 Stern U, Dill DL (1997) Parallelizing the Murϕ verifier. In: Grumberg O (ed) Proceedings of the 9th international conference on computer aided verification, Haifa, Israel, 22–25 June 1997. Lecture notes in computer science, vol 1254, Springer, Berlin Heidelberg New York, pp 256–67