Abstract
In this paper we present a technique to compute abstract models for formal system verification. The method reduces the state space by eliminating those parts of a system model which are not required to check a property. The abstract model depends on the property, which is a formula of the next-less fragment of CTL *. The algorithm reads a system description, annotates it with abstract sub-models for the statements, which are finally composed as abstract model for the system. In the paper we introduce the core algorithm and illustrate it by an example.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alexander Asteroth, Christel Baier, and Ulrich Aßmann. Model checking with formula-dependent abstract models. In Computer Aided Verification (CAV’ 01), 2001.
Felice Balarin and Alberto L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Courcoubetis, editor, Proceedings of Computer Aided Verification (CAV’ 93), volume 697 of Lecture Notes in Computer Science, pages 29–40. Springer, 1993.
Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. In Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 343–354. ACM Press, 1992.
Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999.
Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253–291, 1997.
[HCD+99]_John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng. A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In Proceedings of the International Symposium on Static Analysis (SAS’ 99), 1999.
Michael Jones and Ganesh Gopalakrishnan. Verifying transaction ordering properties in unbounded bus networks through combined deductive/algorithmic methods. In Formal Methods in Computer-Aided Design, pages 505–519, 2000.
Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, and Carl Pixley. Formal verification of FIRE: A case study. In Design Automation Conference, pages 173–177, 1997.
Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, 1994.
[LGS+95]_Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1–35, 1995.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, 1992.
[PVE+00]_John Penix, Willem Visser, Eric Engstrom, Aaron Larson, and Nicholas Weininger. Verification of time partitioning in the DEOS scheduler kernel. In International Conference on Software Engineering, pages 488–497, 2000.
Natalia Sidorova and Martin Steffen. Verification of a wireless atm medium access protocol. Technical Report TR ST 00 3, University of Kiel, Germany, May 2000.
Karen Yorav and Orna Grumberg. Static analysis for state-space reductions preserving temporal logics. Technical Report CS-2000-03, Technion, Israel, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Firley, T., Goltz, U. (2002). Property Dependent Abstraction of Control Structure for Software Verification. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_29
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive