Abstract
Specifications that describe typical scenarios of operations have become common for software applications, using, for example, use-cases of UML. For a system to conform with such a specification, every execution sequence must be equivalent to one in which the specified scenarios occur sequentially, where we consider computations to be equivalent if they only differ in that independent operations may occur in a different order.
A general framework is presented to check the conformance of systems with such specifications using model checking. Given a model and additional information including a description of the scenarios and of the operations’ independence, an augmented model using a transducer and temporal logic assertions for it are automatically defined and model checked. In the augmentation, a small window with part of the history of operations is added to the state variables. New transitions are defined that exchange the order of independent operations, and that identify and remove completed scenarios. If the model checker proves all the generated assertions, every computation is equivalent to some sequence of the specified scenarios. A new technique is presented that allows proving equivalence with a small fixed-size window in the presence of unbounded out-of-order of operations from unrelated scenarios. This key technique is based on the prediction of events, and the use of anti-events to guarantee that predicted events will actually occur. A prototype implementation based on Cadence SMV is described.
This work was partially supported by the Fund for the Support of Research at the Technion.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997)
Braun, T., Condon, A., Hu, A.J., Juse, K.S., Laza, M., Leslie, M., Sharma, R.: Proving sequential consistency by model checking. In: Proc. 6th IEEE High Level Design Validation and Test Workshop (HLDVT 2001), pp. 103–108 (December 2001)
Glusman, M., Katz, S.: A mechanized proof environment for the convenient computations proof method. Formal Methods in System Design (to appear), Available at http://www.cs.technion.ac.il/Labs/ssdl/pub/conv_PVS
Glusman, M., Katz, S.: Mechanizing proofs of computation equivalence. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 354–367. Springer, Heidelberg (1999)
Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying sequential consistency on shared-memory multiprocessor systems. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 301–315. Springer, Heidelberg (1999)
Holzmann, G.J., Peled, D.: The state of SPIN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 385–389. Springer, Heidelberg (1996)
Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distributed Computing 12, 129–149 (1999)
Katz, S.: Refinement with global equivalence proofs in temporal logic. In: Peled, D., Pratt, V., Holzmann, G. (eds.) Partial Order Methods in Verification. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 59–78. American Mathematical Society, Providence (1997)
Katz, S., Peled, D.: Defining conditional independence using collapses. Theoretical Computer Science 101, 337–359 (1992)
Katz, S., Peled, D.: Verification of distributed programs using representative interleaving sequences. Distributed Computing 6, 107–120 (1992)
Kwiatkowska, M.: Fairness for Non-Interleaving Concurrency. PhD thesis, Dept. of Computing Studies, Leicester (1989)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Safety. Springer, Heidelberg (1995)
Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)
McMillan, K.L.: Getting Started With SMV. Cadence Berkley Labs, 2001 Addison St. Berkley, CA (March 1999)
Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)
Valmari, A.: Astubborn attack on state explosion. In: CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1990)
Wolper, P., Godefroid, P.: Partial-ordermethods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Glusman, M., Katz, S. (2003). Model Checking Conformance with Scenario-Based Specifications. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive