Integrating Formal Specification and Software Verification and Validation

  • Roger Duke
  • Tim Miller
  • Paul Strooper
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.


State Machine Formal Method Finite State Machine Assessment Task Graph Class 
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.
    Bloesch, A., Kazmierczak, E., Kearney, P., Staples, J., Traynor, O., Utting, M.: A formal reasoning environment for Sum - a Z based specification language. Technical Report 95-02, Software Verification Research Centre (1995)Google Scholar
  2. 2.
    Carrington, D., MacColl, I., McDonald, J., Murray, L., Strooper, P.: From Object-Z specifications to ClassBench test suites. Journal on Software Testing, Verification and Reliability 10(2), 111–137 (2000)CrossRefGoogle Scholar
  3. 3.
    Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. MacMillan Press Limited, London (2000)Google Scholar
  4. 4.
    Garlan, D.: Making formal methods education effective for professional software engineers. Information and Software Technology 37(3-4), 261–268 (1995)CrossRefGoogle Scholar
  5. 5.
    Gries, D.: The need for education in useful formal logic. IEEE Computer 29(4), 29–30 (1996)Google Scholar
  6. 6.
    Habrias, H., Faucou, S.: Some reflections on the teaching of formal methods. In: Teaching Formal Methods: Practice and Experience (2003),
  7. 7.
    Hazel, D., Strooper, P., Traynor, O.: Possum: An animator for the sum specification language. In: Proceedings Asia-Pacific Software Engineering Conference and International Computer Science Conference, pp. 42–51. IEEE Computer Society, Los Alamitos (1997)CrossRefGoogle Scholar
  8. 8.
    Hazel, D., Strooper, P., Traynor, O.: Requirements engineering and verification using specification animation. In: Proceedings 13th IEEE International Conference on Automated Software Engineering, pp. 302–305. IEEE Computer Society, Los Alamitos (1998)Google Scholar
  9. 9.
    Hinchey, M.G., Bowen, J.P.: To formalize or not to formalize. IEEE Computer 29(4), 18–19 (1996)Google Scholar
  10. 10.
    King, S.: The assessment of students on FM courses: A position paper. In: Teaching Formal Methods: Practice and Experience (2003),
  11. 11.
    Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Chichester (1999)zbMATHGoogle Scholar
  12. 12.
    Maharaj, S.: Formal methods teaching at the University of Stirling. In: Teaching Formal Methods: Practice and Experience (2003),
  13. 13.
    Miller, T., Strooper, P.: A framework for the systematic testing of model-based specifications. ACM Transactions on Software Engineering and Methodology (2004) (to appear)Google Scholar
  14. 14.
    Parnas, D.L.: “formal methods” technology transfer will fail. Journal of Systems and Software 40(3), 195–198 (1998)CrossRefGoogle Scholar
  15. 15.
    Saaltink, M.: The Z/EVES system. In: Proceedings 10th International Conference on the Z Formal Method, pp. 72–88. Springer, Heidelberg (1997)Google Scholar
  16. 16.
    Schneider, S.: The B-Method: An Introduction. Palgrave, Oxford (2001)Google Scholar
  17. 17.
    Sobel, A., Saiedian, S., Stavely, A., Henderson, P.: Teaching formal methods early in the software engineering curriculum. In: Proceedings Thirteenth Conference on Software Engineering Education & Training, p. 55. IEEE Computer Society, Los Alamitos (2000)CrossRefGoogle Scholar
  18. 18.
    Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Transactions on Software Engineering 22(11), 777–793 (1996)CrossRefGoogle Scholar
  19. 19.
    Utting, M., Reeves, S.: Teaching formal methods lite via testing. Software Testing, Verification and Reliability 11(3), 181–195 (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Roger Duke
    • 1
  • Tim Miller
    • 1
  • Paul Strooper
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandBrisbaneAustralia

Personalised recommendations