PICGAL: Practical use of formal specification to develop a complex critical system

  • Lionel Devauchelle
  • Peter Gorm Larsen
  • Henrik Voss
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


This paper reports on the experiment PICGAL which aims to assess the benefits of using VDM to develop high reliability related software in the space industry in a practical way. The application used in this project is a code generator from a next generation environment to be used in the development of ground application software for boosters such as ARIANE V. The experiment is constructed as a parallel development of the code generator; using the conventional approach and using formal specification. This allows detailed measurements of the effects resulting from the introduction of VDM. This work is adding to the existing body of evidence of the effect of using a moderate amount of formal methods in an industrial context in a new critical domain. This paper provides an overview of the domain, the application and it shows how the formal specification has been structured. Finally, results and key lessons are presented.


Code Generator Formal Method Abstract Syntax Control Command Test Coverage 
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. 1.
    John Dawes. The VDM-SL Reference Guide. Pitman, 1991. ISBN 0-273-03151-1.Google Scholar
  2. 2.
    René Elmstrøm, Peter Gorm Larsen, and Poul Bøgh Lassen. The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices, 29(9):77–80, September 1994.Google Scholar
  3. 3.
    John Fitzgerald, Peter Gorm Larsen, Tom Brookes, and Mike Green. Applications of Formal Methods, chapter 14. Developing a Security-critical System using Formal and Convential Methods, pages 333–356. Prentice-Hall International Series in Computer Science, 1995.Google Scholar
  4. 4.
    Brigitte Fröhlich and Peter Gorm Larsen. Combining VDM-SL Specifications with C++ Code. In Marie-Claude Gaudel and Jim Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, pages 179–194. Springer-Verlag, March 1996.Google Scholar
  5. 5.
    Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, Englewood Cliffs, New Jersey, second edition, 1990. ISBN 0-13-880733-7.Google Scholar
  6. 6.
    Peter Gorm Larsen, John Fitzgerald, and Tom Brookes. Applying Formal Specification in Industry. IEEE Software, 13(3):48–56, May 1996.Google Scholar
  7. 7.
    Paul Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, pages 133–140, July 1995.Google Scholar
  8. 8.
    P. G. Larsen and B. S. Hansen and H. Brunn N. Plat and H. Toetenel and D. J. Andrews and J. Dawes and G. Parkin and others. Information technology — Programming languages, their environments and system software interfaces — Vienna Development Method — Specification Language — Part 1: Base language, December 1996.Google Scholar
  9. 9.
    The VDM Tool Group. The IFAD VDM-SL Language. Technical report, IFAD, May 1996. IFAD-VDM-1.Google Scholar
  10. 10.
    T.M. Brookes and J.S. Fitzgerald and P.G. Larsen. Formal and Informal Specifications of a secure System Component: Final Results in a Comparative Study. In Marie-Claude Gaudel and Jim Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, pages 214–227. Springer-Verlag, March 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Lionel Devauchelle
    • 1
  • Peter Gorm Larsen
    • 2
  • Henrik Voss
    • 2
  1. 1.AEROSPATIALE espace et defense, department SY/YI-BP 3 002Mureaux CedexFrance
  2. 2.IFAD (The Institute of Applied Computer Science)Odense MDenmark

Personalised recommendations