Model Checking Z Specifications Using SAL

  • Graeme Smith
  • Luke Wildman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.


model checking SAL tool support 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    de Moura, L., Owre, S., Shankar, N.: The SAL language manual. Technical Report SRI-CSL-01-02 (Rev. 2), SRI International (2003)Google Scholar
  3. 3.
    Derrick, J., Smith, G.: Linear temporal logic and Z refinement. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 117–131. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Duke, R., Rose, G.: Formal Object-Oriented Specification using Object-Z. Cornerstones of Computing. Macmillan, Basingstoke (2000)Google Scholar
  5. 5.
    Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J.v. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 996–1072. Elsevier Science Publishers, Amsterdam (1990)Google Scholar
  6. 6.
    Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) International Conference on Integrated Formal Methods (IFM 1999), pp. 315–334. Springer, Heidelberg (1999)Google Scholar
  8. 8.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  9. 9.
    Hazel, D., Strooper, P., Traynor, O.: Possum: An animator for the SUM specification language. In: Wong, W., Leung, K. (eds.) Asia Pacific Software Engineering Conference (APSEC 1997), pp. 42–51. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  10. 10.
    Jackson, D.: Alloy: A lightweight modelling language. Technical Report 797, MIT Laboratory for Computer Science (2000)Google Scholar
  11. 11.
    Kassel, G., Smith, G.: Model checking Object-Z classes: Some experiments with FDR. In: Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 445–452. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  12. 12.
    Kolyang, K.T., Wolff, B.: A structure preserving encoding of Z in Isabelle/HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming 40, 59–96 (2001)zbMATHCrossRefGoogle Scholar
  14. 14.
    Rueß, H., de Moura, L.: Bounded model checking and induction: From refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Saaltink, M.: The Z-Eves system. In: Till, D., Bowen, J. P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  16. 16.
    Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)zbMATHGoogle Scholar
  17. 17.
    Smith, G., Winter, K.: Proving temporal properties of Z specifications using abstraction. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 260–279. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992), Google Scholar
  19. 19.
    Stringer-Calvert, D., Stepney, S., Wand, I.: Using PVS to prove a Z refinement: A case study. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 573–588. Springer, Heidelberg (1997)Google Scholar
  20. 20.
    Wehrheim, H.: Data abstraction for CSP-OZ. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, p. 1028. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. 21.
    Winter, K., Smith, G.: Compositional verification for Object-Z. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 280–299. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Graeme Smith
    • 1
  • Luke Wildman
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandAustralia

Personalised recommendations