Classification of Formal Specification Methods

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


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 developing 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.


Model Check Temporal Logic Theorem Prove Specification Language Linear Temporal Logic 
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 JR (1996) The b-book—assigning programs to meanings. Cambridge University Press, Cambridge MATHCrossRefGoogle Scholar
  2. 2.
    Alexander M, Gardner W (eds) (2008) Process algebra for parallel and distributed processing. CRC Press, Boca Raton Google Scholar
  3. 3.
    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 MATHCrossRefGoogle Scholar
  4. 4.
    Breen M (2005) Statestep specification technique: user guide, Version 2.0/2005-9-30,
  5. 5.
    ChaoChen Z, Hoare T, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269–276 MathSciNetMATHCrossRefGoogle Scholar
  6. 6.
    Clarke E, Emerson EA (1981) Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of programs: workshop. LNCS, vol 131 Google Scholar
  7. 7.
    Cooke J (1992) Formal methods—mathematics, theory, recipes or what? Comput J 35(5):419–423 MathSciNetCrossRefGoogle Scholar
  8. 8.
    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 Google Scholar
  9. 9.
    Goguen J, Einkler T (1988) Introduction to OBJ3. Technical report, SRI-CSL-88-9, SRI International, Meno Park, CA Google Scholar
  10. 10.
    Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge MATHGoogle Scholar
  11. 11.
    Groote JF (1997) The syntax and semantics of timed CRL. Technical report SEN-R9709, CWI, Amsterdam Google Scholar
  12. 12.
    Guttag JV, Horning JJ, Garland SJ, Jones KD, Modet A, Wing J (1993) Larch: languages and tools for formal specification. Springer, New York MATHCrossRefGoogle Scholar
  13. 13.
    Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8:231–274 MathSciNetMATHCrossRefGoogle Scholar
  14. 14.
    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 CrossRefGoogle Scholar
  15. 15.
    Hoare CAR (1985) Communicating sequential processes. Computer science. Prentice Hall, Englewood Cliffs MATHGoogle Scholar
  16. 16.
    Holzmann G (1991) Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs Google Scholar
  17. 17.
    Iglewski M, Kubica M, Madey J, Mincer-Daszkiewiczb J, Stencel K (2010) TAM’97: the trace assertion method of module interface specification (Reference manual). (June 2010)
  18. 18.
    Luckham DC, von Henke FW, Krieg-Brückner B, Owe O (1987) ANNA: a language for annotating ada programs (reference manual). LNCS, vol 260 MATHCrossRefGoogle Scholar
  19. 19.
    Lynch N, Tuttle M (1989) An introduction to input/output automata. CWI-Quart 2(3):219–246 MathSciNetMATHGoogle Scholar
  20. 20.
    Manna Z, Pnulei A (1992) The temporal logic of reactive and concurrent systems: specifications. Springer, New York CrossRefGoogle Scholar
  21. 21.
    McMillan KL (1993) Symbolic model checking: an approach to state explosion problem. Kluwer Academic, Norwell CrossRefGoogle Scholar
  22. 22.
    Milner R (1980) A calculus of communicating systems. LNCS, vol 92 MATHCrossRefGoogle Scholar
  23. 23.
    Moszkowski B, Manna Z (1983) Reasoning in interval temporal logic. Technical report, Report No STAN-(2-83-969), Stanford University, CA Google Scholar
  24. 24.
    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 Google Scholar
  25. 25.
    Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143–189 MathSciNetMATHCrossRefGoogle Scholar
  26. 26.
  27. 27.
  28. 28.
    Selic B, Gullekson G, Ward PT (1994) Real-time object-oriented modeling. Wiley, New York MATHGoogle Scholar
  29. 29.
    Systä K (2010) DisCo: user manual (draft). (June 2010)
  30. 30.
    Smith G (2000) The object-Z specification language. Kluwer Academic, Norwell MATHCrossRefGoogle Scholar
  31. 31.
    Spivey JM (1992) The Z notation—a reference manual, 2nd edn. Prentice-Hall International, Englewood Cliffs Google Scholar
  32. 32.
  33. 33.
  34. 34.
    Wheeler D (2010) High assurance (for security or safety) and free-libre/open source software (FLOSS). (June 2010)
  35. 35.
    Wing JM (1990) A specifier’s introduction to formal methods. IEEE Comput 23(9):8–24 CrossRefGoogle Scholar
  36. 36.

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