Abstract
Software systems are often model checked by translating them into a directly model-checkable formalism. Any serious software system requires application of compositional reasoning to overcome the computational complexity of model checking. This paper presents Translation-Based Compositional Reasoning (TBCR), an approach to application of compositional reasoning in the context of model checking software systems through model translation. In this approach, given a translation from a software semantics to a directly model-checkable formal semantics, a compositional reasoning rule is established in the software semantics and mapped to an equivalent rule in the formal semantics based on the translation. The correctness proof of the composition reasoning rule in the software semantics is established based on this mapping and the correctness proof of the equivalent rule in the formal semantics. The compositional reasoning rule in the software semantics is implemented and applied based on the translation from the software semantics to the formal semantics and reusing the implementation of the equivalent rule in the formal semantics. TBCR has been realized for a commonly used software semantics, the Asynchronous Interleaving Message-passing semantics. TBCR is illustrated by two applications of this realization.
This research was partially supported by NSF grant 010-3725.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs Workshop (1981)
Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming (1982)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
Pnueli, A.: In transition from global to modular reasoning about programs. Logics and Models of Concurrent Systems (1985)
Alur, R., Henzinger, T.: Reactive modules. In: LICS (1996)
Abadi, M., Lamport, L.: Conjoining specifications. In: TOPLAS (1995)
McMillan, K.L.: Amethodology for hardware verification using compositional model checking. Cadence TR (1999)
Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.: Assume-guarantee based compositional reasoning for synchronous timing diagrams. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 465. Springer, Heidelberg (2001)
de Rover, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge Univ. Press, Cambridge (2001)
Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)
ITU: ITU-T Recommendation Z.100 (03/93) - Specification and Description Language (SDL). ITU (1993)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Hardin, R.H., Har’El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata- Theoretic Approach. Princeton University Press, Princeton (1994)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)
Kurshan, R.P., Merritt, M., Orda, A., Sachs, S.R.: Modeling asynchrony with a synchronous model. Formal Methods in System Design 15(3) (1999)
Xie, F., Browne, J.C.: Integrated state space reduction for model checking executable objectoriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, p. 64. Springer, Heidelberg (2002)
Xie, F., Browne, J.C.: Verified systems by composition from verified components. In: ESEC/FSE (2003)
Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters 21 (1985)
Xie, F., Levin, V., Browne, J.C.: ObjectCheck: a model checking tool for executable objectoriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, p. 331. Springer, Heidelberg (2002)
Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. ASPLOS-IX (2000)
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
Xie, F., Browne, J.C., Kurshan, R.P. (2003). Translation-Based Compositional Reasoning for Software Systems. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive