Abstract
We present a partitioning algorithm for checking ACTL specifications that distinguishes between states only if this is necessary to ascertain the specification. This algorithm is then generalized to also abstract from the variable values in the states. Here, too, the values between which the algorithm distinguishes are determined by what is needed to decide whether or not the specification holds. The resulting algorithm is being implemented in an ROBDD based model checker for VHDL/S.
Currently working in ESPRIT project P6021 “Building Correct Reactive Systems (React)”.
Currently working in ESPRIT project P6128 “Formal Methods in Hardware Design (Format)”.
Currently working in Projekt “Informationssysteme”.
Chapter PDF
References
J. R. Burch, E. M. Clarke, K. L. Mcmillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Anual IEEE Symposium on Logic in Computer Science (LICS), 1990.
A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programmming, 18(3):247–271, 1992.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. Transactions on Computers, C-35:677–691, 1986.
R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by constructing or approximation of fixed points. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages (POPL), pages 238–252. ACM, 1977.
D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In C. Courcoubetis, editor, Proceedings of the Fifth Conference on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: abstractions preserving ∀CTL*, ∃CTL* and CTL*. In Proceedings of PROCOMET, IFIP. North-Holland, 1994. To appear.
R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking, 1994. Submitted.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proceedings of the Sixth Anual IEEE Symposium on Logic in Computer Science (LICS), 1991.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8, 1987.
J. Helbig and P. Kelb. An OBDD representation of statecharts, 1994. To appear in EDAC94.
J. Helbig, R. Schlör, W. Damm, G. Döhmen, and P. Kelb. VHDL/S—integrating statecharts, timing diagrams and VHDL. Microprocessing and Microprogramming, 38:571–580, 1993.
D. Peled. All from one, one for all, on model-checking using representatives. In Proceedings of the Fifth International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, pages 409–423. Springer-Verlag, 1993.
R. Schlör and W. Damm. Specification and verification of system-level hardware designs using timing diagrams. In EDAC93, 1993.
A. Valmari. A stubborn attack on state explosion. In Proceedings of the Second Conference on Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dams, D., Gerth, R., Döhmen, G., Herrmann, R., Kelb, P., Pargmann, H. (1994). Model checking using adaptive state and data abstraction. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_75
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive