Distributed Verification with LoLA

• Autorzy: Schmidt K.
• Języki publikacji: EN

Abstrakty

EN

We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.

Słowa kluczowe

EN

Petri net; state space; distributed verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 2,3
• Strony: 253--262
• Opis fizyczny: bibliogr. 10 poz.

Twórcy

autor

Schmidt K.

• Humboldt-Universität zu Berlin, Institut für Informatik, D-10099 Berlin,

Bibliografia

• 1. [BCM92] J. R. Burch, Edmund M. Clarke, and Kenneth L. McMillan. Symbolic model checking: 10.20 states and beyond. Information and Computation, 98(2), June 1992.
• 2. [CES86] Edmund M. Clarke, E. M. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244 - 263, April 1986.
• 3. [HJJJ84] Huber, A. Jensen, Jepsen, and K. Jensen. Towards reachability trees for high–level petri nets. In Advances in Petri Nets 1984, Lecture Notes on Computer Science 188, pages 215–233, 1984.
• 4. [KM69] R. M. Karp and R. E. Miller. Parallel program schemata. Journ. Computer and System Sciences 4, pages 147-195, May 1969.
• 5. [Sch00] K. Schmidt. Lola – a low level analyzer. Proc. 21th Int. Conf. Application and Theory of Petri nets, LNCS 1825, pages 465-474, 2000.
• 6. [SD97] U. Stern and D.L. Dill. Parallelizing the murphi verifier. Proc. Int. Conf. Computer Aided Verification,
• 7. LNCS 1254, pages 256-267, 1997.
• 8. [Sta91] P. Starke. Reachability analysis of petri nets using symmetries. J. Syst. Anal. Model. Simul., 8:294-303, 1991.
• 9. [Val88] A. Valmari. Error detection by reduced reachability graph generation. Proc. of the 9th European Workshop on Application and Theory of Petri Nets, Venice, 1988.
• 10. [VW86] M.Y. Vardi and P. Wolper. An automate-theoretic approach to to automatic program verification. Proc. IEEE Symp. Logic in Computer Science, pages 332-344, 1986.