Abstract
An exceptionally user-friendly approach to computer-aided validation / verification of concurrent and reactive systems is presented. In it, the user needs not express his verification questions formally in detail. Instead, he specifies a point of view to the system by choosing a subset of its externally observable actions. An automaton abstracts and reduces the behaviour of the system according to the choice, and shows the result graphically on a computer screen. The resulting picture represents all executions of the system, as seen from the chosen point of view. Thus the information in it is as comprehensive as that obtained by ordinary verification. On the other hand, like ordinary testing, the method makes it possible for a system designer to get rapid feedback with ease, to “just try the system and see how it behaves”. The article concentrates on practical and philosophical issues regarding the method and contains a detailed example.
Chapter PDF
Similar content being viewed by others
References
Bochmann, G. v.: Usage of Protocol Development Tools: The Results of a Survey. Proceedings of the 7th International Symposium on Protocol Specification, Testing and Verification (1987), North-Holland 1988.
Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14 1987 pp. 25–59. Also in: The Formal Description Technique LOTOS, North-Holland 1989, pp. 23–73.
Brookes, S. D. & Roscoe, A. W.: An Improved Failures Model for Communicating Processes. Proceedings of the NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag, 1985, pp. 281–305.
Cheung, S. C. & Kramer, J.: Enhancing Compositional Reachability Analysis with Context Constraints. Proceedings of the first ACM SIGSOFT Symposium on the Foundations of Software Engineering, ACM Software Engineering Notes, 18(5) 1993, pp. 115–125.
Craigen, D., Gerhart, S. & Ralston, T.: Formal Methods Reality Check: Industrial Usage. Proceedings of Formal Methods Europe '93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 250–267.
Eloranta, J.: Minimal Transition Systems with Respect to Divergence Preserving Behavioural Equivalences. Doctoral thesis, University of Helsinki, Department of Computer Science, Report A-1994-1, Helsinki, Finland 1994, 162 p.
Feldbrugge, F: Petri Net Tool Overview 1992. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 169–209.
Formal Systems (Europe) Ltd.: Failures Divergence Refinement User Manual and Tutorial, version 1.4 1994.
Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. Computer-Aided Verification '90 (Proceedings of a workshop), AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society 1991, pp. 57–73.
Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.
Inverardi, P. & Priami, C.: Evaluation of Tools for the Analysis of Communicating Systems. EATCS Bulletin 45, October 1991, pp. 158–185.
ISO 8807 International Standard: Information processing systems — Open Systems Interconnection — LOTOS — A formal description technique based on the temporal ordering of observational behaviour International Organization for Standardization 1989, 142 p.
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.
Madelaine, E. & Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. Formal Description Techniques II (Proceedings of FORTE '89), North-Holland 1990, pp. 61–66.
Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.
Peterson, G. L.: Myths about the Mutual Exclusion Problem. Information Processing Letters 12 (3) 1981, pp. 115–116.
Setälä, M. & Valmari, A.: Validation and Verification with Weak Process Semantics. Proceedings of Nordic Seminar on Dependable Computing Systems 1994, Lyngby, Denmark, August 1994, pp. 15–26.
Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI (Proceedings of PSTV '91), North-Holland 1991, pp. 3–18.
Valmari, A.: Compositional State Space Generation. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 427–457. (Earlier version in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 43–62.)
Valmari, A., Kemppainen, J., Clegg, M. & Levanto, M.: Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool. Proceedings of Formal Methods Europe '93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597–616.
Valmari, A.: State of the Art Report: Stubborn Sets. Petri Net Newsletter 46, April 1994, pp. 6–14.
Valmari, A.: Failure-based Equivalences Are Faster Than Many Believe. Structures in Concurrency Theory, Proceedings, Berlin, Germany, May 1995, Springer-Verlag “Workshops in Computing” series 1995, pp. 326–340.
Valmari, A. & Tienari, M.: Compositional Failure-based Semantic Models for Basic LOTOS. Formal Aspects of Computing (1995) 7: 440–468.
Valmari, A., Karsisto, K. & Setälä, M.: Visualisation of Reduced Abstracted Behaviour as a Design Tool. To appear in Proceedings of Fourth Euromicro Workshop on Parallel and Distributed Processing, Braga, Portugal, Jan. 1996, IEEE publ., 8 p.
Wolper, P. & Godefroid, P.: Partial-Order Methods for Temporal Verification. Proceedings of CONCUR '93, Lecture Notes in Computer Science 715, Springer-Verlag 1993, pp. 233–246.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A., Setälä, M. (1996). Visual verification of safety and liveness. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_90
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_90
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive