×

zbMATH — the first resource for mathematics

Model checking RAISE applicative specifications. (English) Zbl 1298.68065
Summary: Ensuring the correctness of a given software component has become a crucial aspect in software engineering and model checking provides an almost fully automatic way of achieving this goal. Due to the scalability problems of the model checking technique, it has become popular to apply it at early stages in the development process, when the size of the model is much smaller than the final code. Properties proved in this way can be shown to hold at the implementation level provided that the final code refines the original specification. In this paper we focus on the main issues for adding model checking functionality to the RAISE specification language (RSL) and present the semantic foundations of our current approach for doing so. We also describe a way to use model checking to verify RAISE confidence conditions, ensuring the soundness and completeness of the results checked in this way. We then present the most interesting details of the implementation of a tool that follows the described approach. Finally, we illustrate the application of the technique with two case studies: a Digital Multiplexed Radio Telephone System and the Mondex electronic purse.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial J-R (1988) The B tool (proof proving tool). In: Bloomfield R, Marshall L, Jones R (eds) VDM 88. VDM: the way ahead. Proceedings of 2nd VDM-Europe symposium, September 1988. Springer, Berlin, pp 86-87 · Zbl 1032.68868
[2] Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York · Zbl 0915.68015
[3] Ahn U, George C (2000) C++ translator for RAISE specification language. Technical report 220 UNU-IIST, November 2000
[4] Bérard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (1998) Systems and software verification, model checking techniques and tools. Springer · Zbl 1002.68029
[5] Burch JR, Clarke EM, Mcmillan KL, Dill DL, Hwang LJ (1990) Symbolic model checking: 10\^{20} states and beyond
[6] Boulton R, Gordon A, Gordon M, Harrison J, Herbert J, Van Tassel J (1992) Experience with embedding hardware description languages in HOL. In: International conference on theorem provers in circuit design: theory, practice and experience, pp 129-156
[7] Butler MJ, Leuschel M, Snook C (2005) Tools for system validation with B abstract machines. In: Proceedings of ASM 2005: 12th international workshop on abstract state machines, Paris
[8] Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: POPL, pp 1-3
[9] Bin E, Ziv A, Ur S (eds) (2007) Hardware and software, verification and testing, second international Haifa verification conference, HVC 2006, Haifa, Israel, October 23-26, 2006. Revised selected papers. Lecture notes in computer science, vol 4383. Springer, Berlin · Zbl 1159.68300
[10] Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new Symbolic Model Verifier. In: Halbwachs N, Peled, D. (eds) Proceedings eleventh conference on computer-aided verification (CAV’99). Lecture notes in computer science, no 1633, Trento, Italy. Springer, pp 495-499 · Zbl 1046.68587
[11] Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Pasareanu CS, Robby, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd international conference on software engineering. ACM Press, pp 439-448
[12] Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge · Zbl 0847.68063
[13] Clarke, EM; Wing, JM, Formal methods: state of the art and future directions, ACM Comput Surveys, 28, 626-643, (1996)
[14] Dan L, Aichernig B (2003) Automatic test case generation for RAISE. Technical report 273, UNU-IIST, January 2003
[15] Durmiendo R, George C (1996) Formal development of a digital mutiplexed radio-telephone system. Research report 67, UNU-IIST, P.O. Box 3058, Macau, Feb 1996
[16] Dasso A, George C (2002) Transforming RSL into PVS. Technical report 256, UNU-IIST, May 2002
[17] Dang Van H, George C, Janowski T, Moore R (2002) Specification case studies in RAISE. FACIT. Springer. ftp://ftp.iist.unu.edu/pub/RAISE/case_studies
[18] de Moura L, Owre S, Rueß H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Computer-aided verification, CAV 2004. Lecture notes in computer science, vol 3114, July 2004. Springer, Boston, pp 496-500
[19] Formal Systems Europe. FDR 2 user manual
[20] Freitas L (2005) Model checking circus. PhD thesis, The Univerisity of York, Oct 2005 · Zbl 1120.68423
[21] Freitas, L; Woodcock, J, State-rich model checking, Innov Syst Softw Eng: NASA J, 2, 49-64, (2006)
[22] Freitas L, Woodcock J (2007) Model checking circus: architecture overview. Technical report, The University of York
[23] George C (2001) RAISE tools user guide. Technical report 227, UNU-IIST, Feb 2001
[24] George C (2003) The development of the RAISE tools. In: Formal methods at the crossroads: from Panacea to foundational support. Lectures notes in computer science, vol 2757. Springer, Berlin
[25] George C, Haxthausen AE (2007) Specification, proof, and model checking of the Mondex electronic purse using RAISE. Technical report 352, UNU-IIST, P.O. Box 3058, Macau, Feb 2007
[26] George, C; Haxthausen, AE, Specification, proof, and model checking of the mondex electronic purse using RAISE, Form Asp Comp, 20, 101-116, (2008)
[27] The RAISE Language Group (1992) The RAISE specification language. Prentice Hall International (UK) · Zbl 1104.68360
[28] The RAISE Method Group (1995) The RAISE development method. Prentice Hall International (UK)
[29] Ha TT (1990) Digital satellite communications. Electronic Engineering Series. McGraw Hill, Singapore
[30] Havelund K (1999) Java PathFinder: a translator from Java to Promela. In: SPIN
[31] Haxthausen AE, Le Bliguet M, Kjær AK (2008) Modelling and verification of railway interlocking systems. In: 15th monterey workshop: foundations of computer software, future trends and techniques for development. Invited paper
[32] Hoare, T; Milner, R, Grand challenges for computing research, Comput J, 48, 49-52, (2005)
[33] Hoare CAR (1985) Communicating sequential processes. Prentice Hall International · Zbl 0637.68007
[34] Hoare, CAR, The verifying compiler: a grand challenge for computing research, J ACM, 50, 63-69, (2003) · Zbl 1032.68868
[35] Hoare T (2006) The ideal of verified software. In: 18th International conference on computer aided verification (CAV2006). Lecture notes in computer science, vol 4144, Seattle, Aug 2006. Springer
[36] Holzmann GJ (2003) The SPIN model checker. Addison-Wesley
[37] Hung DV (2002) Real-time systems development with duration calculus: an overview. Technical report 255, UNU-IIST, P.O. Box 3058, Macau, June 2002. Published in the proceedings for the UNU-IIST 10th anniversary colloquium on formal methods at the crossroads, from Panacea to foundational support. LNCS 2757, Nov 2003. Springer, pp 81-96
[38] Ives B, Earl M (1997) Mondex international: reengineering money. Technical report CRIM CS97/2, London Business School
[39] MasterCard International Incorporated. Mondex
[40] ITSEC. http://en.wikipedia.org/wiki/ITSEC
[41] Jones, C; O’Hearn, PW; Woodcock, J, Verified software: a grand challenge, IEEE Comput, 39, 93-95, (2006)
[42] Kolyang TS, Wolff B (1996) A structure preserving encoding of Z in Isabelle/HOL. In: Higher order logics (TPHOLs 96). Springer
[43] Leuschel M, Butler MJ (2003) ProB: a model checker for B. In: Keijiro A, Gnesi S, Dino M (eds) Proceedings of formal methods Europe 2003, Pisa, Italy, Sept 2003, pp 855-874
[44] Metayer C, Abrial J-R, Voisin L (2005) Event-B language. RODIN Project Deliverable D7, May 2005
[45] Müller, O; Slind, K, Treating partiality in a logic of total functions, Comput J, 40, 640-652, (1997)
[46] Neilson DS, Sorensen IH (1994) The B-Technologies: a system for computer aided programming. In: Proceedings 6th nordic workshop on programming theory, pp 18-35
[47] Perna J, George C (2005) Model checking RAISE specifications. Technical report 331, UNU-IIST, Dec 2005 · Zbl 1298.68065
[48] Perna J, George C (2006) Towards the verification of RAISE specifications through model checking. In: Proceedings of the 8th workshop of researchers in computer sciences, June 2006. ISBN:950-9474-34-7
[49] Pnueli A (1977) The temporal logic of programs. In: 18th IEEE symp. foundations of computer science, New Jersey
[50] Sampaio A (1993) An algebraic approach to compiler design. PhD thesis, Programming Research Group, Oxford University · Zbl 0962.68031
[51] Stringer-Calvert D, Stepney S, Wand I (1997) Using PVS to prove a Z refinement: a case study. In: Formal methods Europe (FME 97). Springer
[52] Spivey JM (1992) The Z notation: a reference manual. Prentice Hall International Series in Computer Science, 2nd edn
[53] Smith G, Wildman L (2005) Model checking Z specifications using SAL. In: ZB 2005. International conference of Z and B users. Springer, pp 85-103 · Zbl 1118.68553
[54] Tapia L, George C (2008) Model checking concurrent RSL with CSPM and FDR2. Research report 393, UNU-IIST, P.O. Box 3058, Macau, April 2008
[55] Tuerk T, Schneider K, Gordon M (2007) Model checking PSL using HOL and SMV. In: Bin E et al (eds) LNCS 4383, pp 1-15
[56] Vargas AP, George C (2008) Formalising the translation from RSL to CSP. Research report 395, UNU-IIST P.O. Box 3058, Macau, May 2008
[57] Vargas AP, Garis AG, Tarifa SLT, George C (2009) Model checking LTL formulae in RAISE with FDR. In: Leuschel M, Wehrheim H (eds) 7th International conference on integrated formal methods (IFM09). LNCS, vol 5423 · Zbl 1211.68252
[58] Vargas AP, Tapia L, George C (2008) A translation from RSL to CSP. In: Proceedings of the Chilean workshop on formal methods, ChWFM
[59] Woodcock J, Cavalcanti A (2001) A concurrent language for refinement. In: 5th Irish workshop on formal methods, Nov 2001
[60] Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River · Zbl 0855.68060
[61] Wei K, George C (2000) An RSL to SML translator. Technical report 208, UNU-IIST, Aug 2000
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.