Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge
Clarke EM, Wing J (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28(4):626–643
Craigen D, Gerhart S, Ralston T (1995) Industrial applications of formal methods to model, design and analyze computer systems
Crow J, De Vitto BL (1996) Formalizing space shuttle software requirements. In: ACM SIGSOFT workshop on formal methods in software practice, San Diego, USA
Dasgupta S (1991) Design theory and computer science. Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge
Derrick J, Boiten E (2002) Combining component specifications in object-Z and CSP. Form Asp Comput, pp 111–127
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
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
Formal methods web page. http://formalmethods.wikia.com/wiki/Z_notation, May 2010
Gordon MJC, Melham TF (eds) (1993) Introduction to HOL. Cambridge University Press, Cambridge
Guttag JV, Horning JJ, Garland SJ, Jones KD, Modet A, Wing JM (1993) Larch: languages and tools for formal specifications. Springer, Berlin
Hartman A AGADIS: model-based generation tools. Technical report. http://www.agedis.de/documents/ModelBasedTestGenerationTools_cs.pdf
Hierons RM (1997) Testing from a Z specification. Softw Test Verif Reliab 7:19–33
Heninger KL et al. (1978) Software requirements for the A-7E aircraft. NRL Report 3876, Naval Research Laboratory
Holloway CM (1999) From bridges and rockets: lessons for software systems. In: 17th international system safety conference, Orlando, Florida, USA, pp 598–607
Alloy DJ (2002) A lightweight object modeling language. ACM Trans Softw Eng Methodol, 11(2):256–290
Jones CB (1990) Systematic software development using VDM, 2nd edn. Prentice-Hall International, Englewood Cliffs
Kapor M (1996) A software design manifesto. In: Winograd T (ed) Bringing design to software. ACM Press, New York, pp 1–9
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
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
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
Rumbaugh J, Blaha M, Pramerlani W, Eddy F, Lorenson W (1991) Object-oriented modeling and design. Prentice-Hall, Englewood Cliffs
Smith G (2000) The object-Z specification language. Kluwer Academic, Norwell
Spivey JM (1988) Understanding Z, a specification language and its formal semantics. Cambridge University Press, Cambridge
Sühl C (2000) Applying RT-Z to develop safety-critical systems. Lecture notes in computer science, vol 1783. Springer, Berlin
TRI-Ada ’94 formal methods panel summary. http://shemesh.larc.nasa.gov/fm/paper-tri-ada.html (04/16/2010)
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
Winograd T (1996) Bringing design to software. Addison Wesley, New York
Wheeler DA (2010) High assurance (for security or safety) and Free-Libre/Open Source Software (FLOSS) …with lots on formal methods/software verification. http://www.dwheeler.com/essays/high-assurance-floss.html (04/16/2010)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2011 Springer-Verlag London Limited
About this chapter
Cite this chapter
Alagar, V.S., Periyasamy, K. (2011). Specification Activities. In: Specification of Software Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-0-85729-277-3_2
Download citation
DOI: https://doi.org/10.1007/978-0-85729-277-3_2
Publisher Name: Springer, London
Print ISBN: 978-0-85729-276-6
Online ISBN: 978-0-85729-277-3
eBook Packages: Computer ScienceComputer Science (R0)