Abstract
Model checking often faces the problem of reducing the large exponential sizes of state-space representations. Several reduction techniques such as bisimulation equivalence, partial-order semantics, and symmetry-based reduction have been proposed, but existing tools do not completely allow a user the flexibility in manipulating state spaces. We propose a new user-friendly verification environment where a user has full control on what techniques to apply and in what sequences to apply them. We have implemented the environment in a tool called State-Graph Manipulators (SGM). SGM packages verification techniques into efficient, reusable, modular manipulators, that act on high-level state-space representations called state-graphs. Further, we are also proposing four new state-space reduction techniques, namely variable shielding, read-write analysis, internal transitions bypassing, and sibling transition multiplicity reduction. They are implemented into SGM and experiments have been conducted to show their usefulness.
Chapter PDF
Similar content being viewed by others
Key words
References
R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, “An implementation of three algorithms for timing verification based on automata emptiness,” In Proc. IEEE Intl Conf Real-Time Systems Symposium, 1992.
R. Alur, C. Courcoubetis, N. Halbwachs, and D. Dill, “Modeling checking for real-time systems,” In Proc IEEE Logics in Computer Science, 1990.
R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi, “Minimization of timed transition systems,” In Proc Intl Conf CONCUR’92, LNCS, volume 630, pages 340354, August 1992.
R. Alur and D. Dill, “Automata for modeling real-time systems,” Theoretical Computer Science, 126 (2): 183–236, April 1994.
J. Bengtsson, F. Larsen, K.Larsson, P. Petterson, Y. Wang, and C. Weise, “New generation of UPPAAL,” In Procs of the Intl Workshop on Software Tools for Technology Transfer (STTT’98), July 1998.
A. Cimatti, F. Clarke, E Giunchiglia, and M. Roveri, “NuSmv: a reimplementation of smv,” In Procs of the Intl Workshop on Software Tools for Technology Transfer (STTT’98), July 1998.
C. Daws, A. Olivers, S. Tripakis, and S. Yovine, “The tools KRONOS,” In Hybrid System III,“ Lecture Notes in Computer Science, volume 1066, pages 208–219, 1996.
C. Daws and S. Yovine, “Reducing the number of clock variables of timed automata,” In Proc Real-Time Systems Symposium, pages 73–81, December 1996.
A. J. Dill, D. L.Drexler, A. J. Hu, and C. H. Yang, “Protocol verification as a hardware design aid,” In Procs of the IEEE Intl Conf on Computer Design: VLSI in Computers and Processors, 1992.
E.A. Emerson and A.P. Sistla, “Utilizing symmetry when model-checking under fairness assumptions: An automata-theoretic approach,” ACM Trans on Programming Languages and Systems, 19 (4): 617–638, July 1997.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking for real-time systems,” In Proc IEEE Logics in Computer Science, 1992.
G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
L. Lamport, “A fast mutual exclusion algorithm,” ACM Trans. on Computer Systems, 5(1):1–11,February 1987.
K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publisher, 1993.
D.A. Peled, “All from one, one for all: On model checking using representatives,” In Proc of the 5th Intl Conf on Computer-Aided Verification, Lecture Notes in Computer Science, volume 697, pages 409–423, 1993.
S. Tripakis and S. Yovine, “Analysis of timed systems based on time-abstracting bisimulations,” In CAV’96, Lecture Notes in Computer Science, volume 1102, 1996.
F. Wang and P.-A. Hsiung, “Automatic verification on the large,” In Proc 3rd IEEE High-Assurance Systems Engineering Symposium (HASE’98), November 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Hsiung, PA., Wang, F. (1999). User-Friendly Verification. In: Wu, J., Chanson, S.T., Gao, Q. (eds) Formal Methods for Protocol Engineering and Distributed Systems. PSTV FORTE 1999 1999. IFIP Advances in Information and Communication Technology, vol 28. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35578-8_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-35578-8_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5270-0
Online ISBN: 978-0-387-35578-8
eBook Packages: Springer Book Archive