Abstract
Verification of parameterized systems for an arbitrary number of instances is generally undecidable. Existing approaches resort to non-trivial restrictions on the system or lack automation. In practice, applications can often provide a suitable bound on the parameter size. We propose a new technique toward the bounded formulation of parameterized reasoning: how to efficiently verify properties of a family of systems over a large finite parameter range. We show how to accomplish this with a single verification run on a model that aggregates the individual instances. Such a run takes significantly less time than if the systems were considered one by one. Our method is applicable to a completely inhomogeneous family of systems, where properties may not even be preserved across instances. In this case the method exposes the parameter values for which the verification fails. If symmetry is present in the systems, it is inherited by the aggregate representation, allowing for verification over a reduced model. Our technique is fully automatic and requires no approximation.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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.
References
Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters (IPL) (1986)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritized fifo resource management. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 174–190. Springer, Heidelberg (2003)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers (1986)
Clarke, E.M., Allen Emerson, E.: The design and synthesis of synchronization skeletons using temporal logic. In: Logic of Programs (LOP) (1981)
Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design (FMSD) (1996)
Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Principles of Distributed Computing (PODC) (1987)
Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Principles of Distributed Computing (PODC) (1986)
Ching-Tsun, C., Mannava, P.K., Seungjoon, P.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004)
Allen Emerson, E., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming (SOCP) (1982)
Allen Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: Computer-Aided Design (CAD) (2000)
Allen Emerson, E., Kahlon, V.: Model checking large-scale and parameterized resource allocation systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 251. Springer, Heidelberg (2002)
Allen Emerson, E.: Temporal and model logic. In: Handbook of Theoretical Computer Science. North-Holland Pub. Co./MIT Press (1990)
Allen Emerson, E., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Allen Emerson, E., Prasad Sistla, A.: Symmetry and model checking. In: Formal Methods in System Design (FMSD) (1996)
Allen Emerson, E., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216–230. Springer, Heidelberg (2003)
German, S.M., Prasad Sistla, A.: Reasoning about systems with many processes. Journal of the ACM (1992)
Norris Ip, C., Dill, D.L.: Verifying systems with replicated components in Murφ. Formal Methods in System Design (FMSD) (1999)
Kumar, V., Grama, A., Gupta, A., Karypis, G.: Introduction to Parallel Computing. Benjamin/Cummings Publishing (1994)
Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Principles of distributed computing (PODC) (1989)
Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs. Acta Informatica (1984)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)
Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. Transactions on Computer Systems (TOCS) (1991)
Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
Quielle, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: 5th International Symposium on Programming (1982)
Somenzi, F.: The CU Decision Diagram Package, release 2.3.1. University of Colorado at Boulder, http://vlsi.colorado.edu/~fabio/CUDD/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Trefler, R.J., Wahl, T. (2006). Reducing Model Checking of the Few to the One. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_6
Download citation
DOI: https://doi.org/10.1007/11901433_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)