Specification Activities

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)


The previous chapter provides a general discussion of the different stages of specification in the software development process. It was assumed that the discrete steps of the development process have been well-defined. That is, the activities, deliverables, reviews, and analysis procedures associated with each step have already been established. It was suggested that a specification of the products and processes can be added to each step of such a well-defined development process. This chapter addresses specific issues that should be considered, activities that should be initiated, and the roles that are to be assumed when specifications are formal due to the integration of formal methods into the existing software life-cycle process for a given project.


Formal Method Design Team Software Development Process Semantic Domain Automate Teller Machine 
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.


  1. 1.
    Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge MATHCrossRefGoogle Scholar
  2. 2.
    Clarke EM, Wing J (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28(4):626–643 CrossRefGoogle Scholar
  3. 3.
    Craigen D, Gerhart S, Ralston T (1995) Industrial applications of formal methods to model, design and analyze computer systems Google Scholar
  4. 4.
    Crow J, De Vitto BL (1996) Formalizing space shuttle software requirements. In: ACM SIGSOFT workshop on formal methods in software practice, San Diego, USA Google Scholar
  5. 5.
    Dasgupta S (1991) Design theory and computer science. Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge CrossRefGoogle Scholar
  6. 6.
    Derrick J, Boiten E (2002) Combining component specifications in object-Z and CSP. Form Asp Comput, pp 111–127 Google Scholar
  7. 7.
    Dick J, Faivre A (1993) Automating the generation and sequencing of test cases from model-based specifications. In: Woodcock JCP, Larsen PG (eds) FME93: industrial-strength formal methods, formal methods Europe. Lecture notes in computer science, vol 670. Springer, Berlin Google Scholar
  8. 8.
    De Vito BL, Roberts L (1996) Using formal methods to assist in the requirements analysis of the space shuttle GPS change request. NASA Report 4752, Prepared for Langley Research Center Google Scholar
  9. 9.
    Formal methods web page., May 2010
  10. 10.
    Gordon MJC, Melham TF (eds) (1993) Introduction to HOL. Cambridge University Press, Cambridge MATHGoogle Scholar
  11. 11.
    Guttag JV, Horning JJ, Garland SJ, Jones KD, Modet A, Wing JM (1993) Larch: languages and tools for formal specifications. Springer, Berlin MATHCrossRefGoogle Scholar
  12. 12.
    Hartman A AGADIS: model-based generation tools. Technical report.
  13. 13.
    Hierons RM (1997) Testing from a Z specification. Softw Test Verif Reliab 7:19–33 CrossRefGoogle Scholar
  14. 14.
    Heninger KL et al. (1978) Software requirements for the A-7E aircraft. NRL Report 3876, Naval Research Laboratory Google Scholar
  15. 15.
    Holloway CM (1999) From bridges and rockets: lessons for software systems. In: 17th international system safety conference, Orlando, Florida, USA, pp 598–607 Google Scholar
  16. 16.
    Alloy DJ (2002) A lightweight object modeling language. ACM Trans Softw Eng Methodol, 11(2):256–290 CrossRefGoogle Scholar
  17. 17.
    Jones CB (1990) Systematic software development using VDM, 2nd edn. Prentice-Hall International, Englewood Cliffs MATHGoogle Scholar
  18. 18.
    Kapor M (1996) A software design manifesto. In: Winograd T (ed) Bringing design to software. ACM Press, New York, pp 1–9 Google Scholar
  19. 19.
    Formal methods specification and verification guidebook for software and computer systems, vol I: Planning and technology insertion. NASA Report NASA-GB-002-95, Release 1.0, July 1995 Google Scholar
  20. 20.
    Formal methods specification and analysis guidebook for the verification of software and computer systems, vol II: A practitioner’s companion. NASA Report NASA-GB-001-97, Release 1.0, May 1997 Google Scholar
  21. 21.
    Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) Proceedings of the eleventh international conference on automated deduction (CADE), Saratoga, New York, June 1992. Lecture notes in artificial intelligence, vol 607. Springer, Berlin, pp 748–752 Google Scholar
  22. 22.
    Rumbaugh J, Blaha M, Pramerlani W, Eddy F, Lorenson W (1991) Object-oriented modeling and design. Prentice-Hall, Englewood Cliffs Google Scholar
  23. 23.
    Smith G (2000) The object-Z specification language. Kluwer Academic, Norwell MATHCrossRefGoogle Scholar
  24. 24.
    Spivey JM (1988) Understanding Z, a specification language and its formal semantics. Cambridge University Press, Cambridge MATHGoogle Scholar
  25. 25.
    Sühl C (2000) Applying RT-Z to develop safety-critical systems. Lecture notes in computer science, vol 1783. Springer, Berlin Google Scholar
  26. 26.
    TRI-Ada ’94 formal methods panel summary. (04/16/2010)
  27. 27.
    van Schouwen AJ (1990) The A-7 requirements model: re-examination of real-time systems and an application to monitoring systems. Technical report 90-276, Department of Computing and Information Science, Queens University, Kingston, Canada Google Scholar
  28. 28.
    Winograd T (1996) Bringing design to software. Addison Wesley, New York Google Scholar
  29. 29.
    Wheeler DA (2010) High assurance (for security or safety) and Free-Libre/Open Source Software (FLOSS) …with lots on formal methods/software verification. (04/16/2010)

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations