Extending Formal Methods for Software-Intensive Systems

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


Formal methods have proven beneficial in the industrial development of software-intensive systems; not in replacing traditional engineering methods, but in complementing them. They provide means of checking for ambiguities and inconsistencies in requirements, as well as verifying safety and liveness properties, and the correctness of designs.

As complexity increases, the formal methods employed need to deal with a number of concerns. Primarily they need to be able to model a diverse range of software and hardware components. Ideally, they should also be capable of supporting requirement changes allowing ‘ideal’ functional specifications to be transformed to reflect actual implementations. Additionally, they should support the introduction of architectural design into functional specifications; including designs involving complex dynamic architectures.

This paper proposes one approach to deal with these concerns. The approach builds on and combines three separate areas of research on integrating formal methods, formal requirements development and formal design derivation. Developing more general theories and techniques that can be applied across a wide range of formal notations remains a significant research challenge.


Formal Method MultiAgent System Architectural Design Process Algebra Liveness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  2. 2.
    Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Science of Computer Programming 67(2-3), 301–329 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Boulton, R., Gottliebsen, H., Hardy, R., Kelsey, T., Martin, U.: Design verification for control engineering. In: Boiten, E., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 21–35. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40, 269–271 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Davies, J., Schneider, S.: A brief history of Timed CSP. Theoretical Computer Science 138(2), 243–271 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  7. 7.
    Derrick, J., Boiten, E.: Refinement in Z and Object-Z, Foundations and Advanced Applications. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  8. 8.
    Derrick, J., Smith, G.: Structural refinement of systems specified in Object-Z and CSP. Formal Aspects of Computing 15(1), 1–27 (2003)CrossRefzbMATHGoogle Scholar
  9. 9.
    Duke, R., Rose, G., Smith, G.: Transferring formal techniques to industry: A case study. In: Quemada, J., Mañas, J., Vazquez, E. (eds.) Formal Description Techniques (FORTE 1990), pp. 279–286. North-Holland, Amsterdam (1990)Google Scholar
  10. 10.
    Fidge, C.J., Hayes, I.J., Mahony, B.P.: Defining differentiation and integration in Z. In: Staples, J., Hinchey, M.G., Liu, S. (eds.) International Conference on Formal Engineering Methods (ICFEM 1998), pp. 64–73. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  11. 11.
    Fidge, C.J., Hayes, I.J., Martin, A.P., Wabenhorst, A.K.: A set-theoretic model for real-time specification and reasoning. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 188–206. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Fischer, C., Wehrheim, H.: Failure-divergence semantics as a formal basis for an object-oriented integrated formal method. Bulletin of the EATCS 71, 92–101 (2000)zbMATHGoogle Scholar
  13. 13.
    Gruer, P., Hilaire, V., Koukam, A., Cetnarowicz, K.: A formal framework for multi-agent systems analysis and design. Expert System Applications 23(4), 349–355 (2002)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hayes, I.J., Jackson, M., Jones, C.B.: Determining the specification of a control system from that of its environment. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 154–169. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  16. 16.
    Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: a combination of specification techniques for processes, data and time. Nordic Journal of Computing 9(4), 301–334 (2002)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Karkinsky, D., Schneider, S., Treharne, H.: Combining mobility with state. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 373–392. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2), 150–177 (2000)CrossRefGoogle Scholar
  19. 19.
    Mahony, B.P., Dong, J.S.: Sensors and actuators in TCOZ. In: Wing, J., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1166–1185. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  20. 20.
    Mahony, B.P., Hayes, I.J.: A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering 18(9), 817–826 (1992)CrossRefGoogle Scholar
  21. 21.
    McComb, T.: Refactoring Object-Z specifications. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 69–83. Springer, Heidelberg (2004)Google Scholar
  22. 22.
    McComb, T.: Formal Derivation of Object-Oriented Designs. PhD thesis, The University of Queensland (2007)Google Scholar
  23. 23.
    McComb, T., Smith, G.: Architectural design in Object-Z. In: Strooper, P. (ed.) Australian Software Engineering Conference (ASWEC 2004), pp. 77–86. IEEE Computer Society Press, Los Alamitos (2004)CrossRefGoogle Scholar
  24. 24.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  25. 25.
    Milner, R.: Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  26. 26.
    Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  27. 27.
    Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J., Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  28. 28.
    Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)CrossRefzbMATHGoogle Scholar
  29. 29.
    Smith, G.: Stepwise development from ideal specifications. In: Edwards, J. (ed.) Australasian Computer Science Conference (ACSC 2000). Australian Computer Science Communications, vol. 22, pp. 227–233. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  30. 30.
    Smith, G.: An integration of Real-Time Object-Z and CSP for specifying concurrent real-time systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 267–285. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  31. 31.
    Smith, G.: A formal framework for modelling and analysing mobile systems. In: Australasian Computer Science Conference (ASCS 2004), pp. 193–202. Australian Computer Society (2004)Google Scholar
  32. 32.
    Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design 18, 249–284 (2001)CrossRefzbMATHGoogle Scholar
  33. 33.
    Smith, G., Fidge, C.: Incremental development of real-time requirements: The light control case study. Journal of Universal Computer Science 6(7), 704–730 (2000)Google Scholar
  34. 34.
    Smith, G., Hayes, I.J.: An introduction to Real-Time Object-Z. Formal Aspects of Computing 13(2), 128–141 (2002)CrossRefzbMATHGoogle Scholar
  35. 35.
    Taguchi, K., Dong, J.S., Ciobanu, G.: Relating pi-calculus to Object-Z. In: International Conference on Engineering of Complex Computer Systems (ICECCS 2004), pp. 97–106. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  36. 36.
    Wildman, L.: Requirements reformulation using formal specification: a case study. In: Lakos, C., Esser, R., Bristensen, L.M., Billington, J. (eds.) Workshop on the use of Formal Methods in Defence Systems, pp. 75–83. Australian Computer Society (2002)Google Scholar
  37. 37.
    Wooldridge, M.: An Introduction to MultiAgent Systems. John Wiley & Sons, Chichester (2002)Google Scholar
  38. 38.
    Zakiuddin, I., Goldsmith, M., Whittaker, P., Gardiner, P.: A methodology for model-checking ad-hoc networks. In: Ball, T., Rajamani, S. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 181–196. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

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

Personalised recommendations