Abstract
A new on-the-fly verification method is presented. The method uses a generalization of Büchi automata called “tester processes” for representing and detecting illegal behaviour. To reduce the number of states that are constructed the method applies the stubborn set theory in a new way. The method can be used in connection with the “Supertrace” memory-saving technique. A simple algorithm is suggested for efficient detection of violations of an important subclass of liveness properties during the construction of the reduced state space.
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.
Referenes
Aho, A. V.; Hopcroft, J. E. & Ullman, J. D.: The Design and Analysis of Computer Algorithms. Addison-Wesley 1974, 470 p.
Brinksma, E.: A Theory for the Derivation of Tests. Protocol Specification, Testing and Verification VIII (Proceedings of International IFIP WG 6.1 Symposium, 1988), North-Holland 1988, pp. 63–74.
Courcoubetis, C.; Vardi, M.; Wolper, P. & Yannakakis, M.: Memory Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design, 1: 275–288 (1992). (An earlier version appeared in Workshop on Computer-Aided Verification, New Brunswick, NJ, USA 1990.)
Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science Volume 3, 1991, pp. 321–340. (An earlier version appeared in Workshop on Computer-Aided Verification, New Brunswick, NJ, USA 1990.)
Godefroid, P. & Wolper, P.: A Partial Approach to Model Checking. Proceedings of the 6th IEEE Symposium on Logic in Computer Science, Amsterdam, July 1991, pp. 406–415.
Godefroid, P. & Wolper, P.: Using Partial Orders for the Efficient Checking of Deadlock Freedom and Safety Properties. Proceedings of 3rd Workshop on Computer-Aided Verification 1991, Lecture Notes in Computer Science 575, Springer-Verlag 1992, pp. 332–342.
Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.
Holzmann, G. J.: Design and Validation of Computer Protocols. Prentice-Hall 1991, 500 p.
Holzmann, G. J.; Godefroid, P. & Pirottin, D.: Coverage Preserving Reduction Strategies for Reachability Analysis. 14 p., Participant's Proceedings of the 12th International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, Florida, USA, 1992.
Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. Proceedings of CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.
Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95–112.
Valmari, A.: Eliminating Redundant Interleavings during Concurrent Program Verification. Proceedings of Parallel Architectures and Languages Europe '89, Lecture Notes in Computer Science 366, Springer-Verlag 1989, pp. 89–103.
Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491–515. (An earlier version appeared in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, Germany 1989, Vol. II pp. 1–22.)
Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design, 1: 297–322 (1992). (An earlier version appeared in Workshop on Computer-Aided Verification, New Brunswick, NJ, USA 1990.)
Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI (Proceedings of International IFEP WG 6.1 Symposium, Stockholm, Sweden 1991), North-Holland 1991, pp. 3–18.
Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. University of Helsinki, Department of Computer Science, Report A-1992-4, Helsinki 1992, 57 p.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A. (1993). On-the-fly verification with stubborn sets. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_33
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive