A Pragmatic Approach to Formal Specification

  • Maritta Heisel
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 371)


We propose a pragmatic approach to overcome some difficulties arising in the practical usage of formal specification techniques. We argue that the transition from informal requirements to a formal specification should not be made too early, that it is not necessary to formally specify every detail, that different formalisms should be combined where appropriate, and that sometimes it may be useful not to adhere to limitations imposed by the formal specification language. This pragmatic approach also helps to deal with legacy systems.


Formal Specification Legacy System Specification Language Pragmatic Approach Generate Test Case 
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. [BGM89]
    M. Bidoit, M.-C. Gaudel, and A. Mauboussin. How to make algebraic specifications more understandable: An experiment with the PLUSS specification language. Science of Computer Programming, 12:1–38, 1989.MATHCrossRefGoogle Scholar
  2. [Bro87]
    Frederick P. Brooks. No silver bullet — essence and accidents of software engineering. Computer, pages 10–19, April 1987.Google Scholar
  3. [DS95]
    Jim Davies and Steve Schneider. Real-time CSP. In Teodor Rus and Charles Rattray, editors, Theories and Experiences for Real-Time System Development. World Scientific Publishing Company, 1995.Google Scholar
  4. [GHJV95]
    Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns — Elements of Reusable Object-Oriented Software. Addison Wesley, 1995.Google Scholar
  5. [Har87]
    David Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.MATHCrossRefGoogle Scholar
  6. [Hei95a]
    Maritta Heisel. Six steps towards provably safe software. In G. Rabe, editor, Proceedings of the 14th International Conference on Computer Safety, Reliability and Security, Belgirate, Italy, pages 191–205, London, 1995. Springer.Google Scholar
  7. [Hei95b]
    Maritta Heisel. Specification of the Unix file system: A comparative case study. In V.S. Alagar and Maurice Nivat, editors, Proc. 4th Int. Conference on Algebraic Methodology and Software Technology, LNCS 936, pages 475–488. Springer-Verlag, 1995.Google Scholar
  8. [HK91]
    Iain Houston and Steve King. CICS project report. Experiences and results from the use of Z in IBM. In VDM’91: Formal Software Development Methods. Symposium of VDM Europe, Noordwijkerhout, LNCS 551, pages 588–596, Berlin, 1991. Springer Verlag.Google Scholar
  9. [HK95a]
    Maritta Heisel and Balachander Krishnamurthy. Bi-directional approach to modeling architectures. Technical Report 95-31, TU Berlin, 1995.Google Scholar
  10. [HK95b]
    Maritta Heisel and Balachander Krishnamurthy. YEAST — a formal specification case study in Z. Technical Report 95-32, TU Berlin, 1995.Google Scholar
  11. [HP95]
    Hans-Martin Horcher and Jan Peleska. Using formal specifications to support software testing. Software Quality Journal, 4(4), 1995.Google Scholar
  12. [ITS91]
    ITSEC. Information technology security evaluation criteria. Commission of the European Union, 1991.Google Scholar
  13. [JZ95]
    Michael Jackson and Pamela Zave. Deriving specifications from requirements: an example. In Proceedings 11th Int. Conf. on Software Engineering, Seattle, USA, pages 15–24. ACM Press, 1995.Google Scholar
  14. [Pel95]
    Jan Peleska. Formal Methods and the Development of Dependable Systems. University of Kiel, Habilitation thesis, 1995.Google Scholar
  15. [Spi92]
    J. M. Spivey. The Z Notation — A Reference Manual. Prentice Hall, 2nd edition, 1992.Google Scholar
  16. [Süh96]
    Carsten Sühl. Eine Methode für die Entwicklung von Softwarekomponen-ten zur Steuerung und Kontrolle sichereitsrelevanter Systeme. Master’s thesis, Technical University of Berlin, 1996.Google Scholar
  17. [Web96]
    Matthias Weber. Combining Statecharts and Z for the design of safety-critical systems. In M.-C. Gaudel and J. Woodcock, editors, FME’ 96 — Industrial Benefits and Advances in Formal Methods, LNCS 1051, pages 307–326. Springer Verlag, 1996.Google Scholar
  18. [Wir90]
    Martin Wirsing. Algebraic specification. In J. von Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 675–788. Elsevier, 1990.Google Scholar
  19. [ZJ93]
    Pamela Zave and Michael Jackson. Conjunction as composition. ACM Transactions on Software Engineering and Methodology, 2(4):379–411, October 1993.CrossRefGoogle Scholar

Copyright information

© Kluwer Academic Publishers 1996

Authors and Affiliations

  • Maritta Heisel
    • 1
  1. 1.Technische Universität BerlinBerlinGermany

Personalised recommendations