Abstract
This paper presents a systematic consideration of the major issues involved in translation of executable design level software specification languages to directly model-checkable formal languages. These issues are considered under the framework of integrated model/property translation and include: (1) translator architecture; (2) semantics translation from a software language to a formal language; (3) property specification and translation; (4) transformations for state space reduction; (5) translator validation and evolution. Solutions to these issues are defined, described, and illustrated in the context of translating xUML, an executable design level software specification language, to S/R, the input formal language of the COSPAN model checker.
This research was partially supported by NSF grant 010-3725.
Chapter PDF
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)
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Roby: Bandera: a source-level interface for model checking Java programs. In: ICSE (2000)
Havelund, K., Skakkebæk, J.U.: Applying Model Checking in Java Verification. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 216. Springer, Heidelberg (1999)
Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE TSE 28 (2002)
Lilius, J., Porres, I.: vUML: a tool for verifying UML models. In: ASE (1999)
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)
Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)
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)
Levin, V., Yenigün, H.: SDLCheck: A model checking tool. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 378. Springer, Heidelberg (2001)
ITU: ITU-T Recommendation Z.100 (03/93) - Specification and Description Language (SDL). ITU (1993)
Sharygina, N., Browne, J.C.: Model checking software via abstraction of loop transitions. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 325–340. Springer, Heidelberg (2003)
Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 345. Springer, Heidelberg (1998)
Holzmann, G.J.: The model checker SPIN. TSE 23(5) (1997)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Namjoshi, K., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Kurshan, R.P.: FormalCheck User’s Manual (1998)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. Formal Methods in Software Practice (1998)
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)
Kurshan, R.P., Levin, V., Yenigün, H.: Compressing transitions for model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 569. Springer, Heidelberg (2002)
Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: FMSD (1996)
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531. Springer, Heidelberg (1991)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Xie, F., Browne, J.C., Kurshan, R.P.: Translation-based compositional reasoning for software systems. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805. Springer, Heidelberg (2003)
Pnueli, A., Siegel, M.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 151. Springer, Heidelberg (1998)
Kapoor, C., Tesar, D.: A reusable operational software architecture for advanced robotics (OSCAR). The University of Texas at Austin, Report to U.S. Dept. of Energy, Grant No. DE-FG01 94EW37966 and NASA Grant No. NAG 9-809 (1998)
Wang, W., Hidvegi, Z., Bailey, A.D., Whinston, A.B.: E-processes design and assurance using model checking. IEEE Computer 33 (2000)
Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In: ASPLOS-IX (2000)
Sharygina, N., Browne, J.C., Kurshan, R.P.: Formal object-oriented analysis for software reliability design for verification. In: FASE (2001)
Xie, F., Browne, J.C.: Integrated state space reduction for model checking executable object-oriented 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)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems 14 (1988)
Gnesi, S., Latella, D., Massink, M.: Model checking UML statechart diagrams using JACK. In: HASE (1999)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in Promela/Spin. In: Industrial Strength Formal Specification Technologies (1993)
Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. PSTV (1990)
Bozga, M., Graf, S., Mounier, L.: Automated validation of distributed software using the IF environment. In: CAV (2001)
Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J., Mounier, L., Sifakis, J.: IF: An intermediate representation for SDL and its applications. In: SDL-Forum 1999 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xie, F., Levin, V., Kurshan, R.P., Browne, J.C. (2004). Translating Software Designs for Model Checking. In: Wermelinger, M., Margaria-Steffen, T. (eds) Fundamental Approaches to Software Engineering. FASE 2004. Lecture Notes in Computer Science, vol 2984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24721-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-24721-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21305-5
Online ISBN: 978-3-540-24721-0
eBook Packages: Springer Book Archive