Abstract
Formal specification methods use languages with mathematically defined syntax and semantics, and offer methods to describe systems and their properties. The strength of a formal method rests on the level of formality and expressiveness afforded by its specification language, and availability of tools that support the method for develo** the system in strict conformance to the system specification. So, a formal method may be placed in its category depending upon its strength and practical use, which in turn depend on the four pillars mathematical basis, type of systems, level of formality, and tools support.
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
Similar content being viewed by others
References
Abrial JR (1996) The b-book—assigning programs to meanings. Cambridge University Press, Cambridge
Alexander M, Gardner W (eds) (2008) Process algebra for parallel and distributed processing. CRC Press, Boca Raton
Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. An EATCS series, vol XXV. Springer, Berlin
Breen M (2005) Statestep specification technique: user guide, Version 2.0/2005-9-30, http://statestep.com
ChaoChen Z, Hoare T, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269–276
Clarke E, Emerson EA (1981) Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of programs: workshop. LNCS, vol 131
Cooke J (1992) Formal methods—mathematics, theory, recipes or what? Comput J 35(5):419–423
Dill DL, Drexler AJ, Hu AJ, Yang CH (1992) Protocol verification as a hardware design aid. In: IEEE international conference on computer design: VLSI in computers and processors. IEEE Computer Society, Los Alamitos, pp 522–525
Goguen J, Einkler T (1988) Introduction to OBJ3. Technical report, SRI-CSL-88-9, SRI International, Meno Park, CA
Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge
Groote JF (1997) The syntax and semantics of timed CRL. Technical report SEN-R9709, CWI, Amsterdam
Guttag JV, Horning JJ, Garland SJ, Jones KD, Modet A, Wing J (1993) Larch: languages and tools for formal specification. Springer, New York
Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8:231–274
Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtull-Trauring R, Trakhtenbrot M (1990) Statemate: a working environment for the development of complex reactive systems. IEEE Trans Softw Eng 16(4):403–414
Hoare CAR (1985) Communicating sequential processes. Computer science. Prentice Hall, Englewood Cliffs
Holzmann G (1991) Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs
Iglewski M, Kubica M, Madey J, Mincer-Daszkiewiczb J, Stencel K (2010) TAM’97: the trace assertion method of module interface specification (Reference manual). http://w3.uqo.ca/iglewski/public_html/TAM/SRC/tam-1.html (June 2010)
Luckham DC, von Henke FW, Krieg-Brückner B, Owe O (1987) ANNA: a language for annotating ada programs (reference manual). LNCS, vol 260
Lynch N, Tuttle M (1989) An introduction to input/output automata. CWI-Quart 2(3):219–246
Manna Z, Pnulei A (1992) The temporal logic of reactive and concurrent systems: specifications. Springer, New York
McMillan KL (1993) Symbolic model checking: an approach to state explosion problem. Kluwer Academic, Norwell
Milner R (1980) A calculus of communicating systems. LNCS, vol 92
Moszkowski B, Manna Z (1983) Reasoning in interval temporal logic. Technical report, Report No STAN-(2-83-969), Stanford University, CA
Owre S, Shankar N, Rushby JM, Stringer-Calvert DWJ (1999) PVS system guide, version 2.3. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA
Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143–189
ProofPower. http://www.lemma-one.com/ProofPower/index/index.html
RODIN project. http://www.bmethod.com/php/travaux-r&d-methode-b-projet-RODIN-en.php
Selic B, Gullekson G, Ward PT (1994) Real-time object-oriented modeling. Wiley, New York
Systä K (2010) DisCo: user manual (draft). http://disco.cs.tut.fi/animation/disco92/disco_tool_manual.fm.html (June 2010)
Smith G (2000) The object-Z specification language. Kluwer Academic, Norwell
Spivey JM (1992) The Z notation—a reference manual, 2nd edn. Prentice-Hall International, Englewood Cliffs
VDM portal. http://www.vdmportal.org/twiki/bin/view
Wheeler D (2010) High assurance (for security or safety) and free-libre/open source software (FLOSS). http://www.dwheeler.com/essays/high-assurance-floss.html (June 2010)
Wing JM (1990) A specifier’s introduction to formal methods. IEEE Comput 23(9):8–24
Z notation. http://formalmethods.wikia.com/wiki/Z_notation
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). Classification of Formal Specification Methods. In: Specification of Software Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-0-85729-277-3_8
Download citation
DOI: https://doi.org/10.1007/978-0-85729-277-3_8
Publisher Name: Springer, London
Print ISBN: 978-0-85729-276-6
Online ISBN: 978-0-85729-277-3
eBook Packages: Computer ScienceComputer Science (R0)