Dear Sir, Yours faithfully: an Everyday Story of Formality

  • Peter Amey
Conference paper


The paper seeks a perspective on the reality of Formal Methods in industry today. What has worked; what has not; and what might the future bring? We show that where formality has been adopted it has largely been benefical. We show that formality takes many forms, not all of them obviously “Formal Methods”.


Model Check Formal Method Formal Verification Mathematical Rigour Cost Overrun 
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. [Amey 2002]
    Peter Amey. Correctness by Construction: Better Can Also Be Cheaper. CrossTalk Magazine, March 2002.Google Scholar
  2. [Bames 2003]
    John Bames. High Integrity Software - the SPARK Approach to Safety and Security. Addison Wesley Longman, ISBN 0-321-13616-0.Google Scholar
  3. [Butler 1993]
    Butler, Ricky W.; and Finelli, George B. The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, vol. 19, no. 1, Jan. 1993, pp 3–12.CrossRefGoogle Scholar
  4. [Calero 1997]
    J Calero, C Roman and G D Palma. A practical design case using formal verification. In Proceedings of Design-SuperCon97.Google Scholar
  5. [DePalma 1996]
    G. DePalma and A. Glaser 1996. Formal verification augments simulation. Electrical Engineering Times 56.Google Scholar
  6. [Hall 1990]
    Anthony Hall. Seven Myths of Formal Methods. IEEE Software, September 1990, pp 11–19.Google Scholar
  7. [Hall 1996]
    Anthony Hall. Using formal methods to develop an ATC information system. IEEE Software 13(2): pp 66–76, 1996.CrossRefGoogle Scholar
  8. [Hall 2002a]
    Anthony Hall. Correctness by Construction: Integrating Formality into a Commercial Development Process. FME 2002: Formal Methods - Getting IT Right, LNCS 2391, Springer Verlag, pp 224–233.Google Scholar
  9. [Hall 2002b]
    Anthony Hall and Roderick Chapman. Correctness by Construction: Developing a Commercial Secure System. IEEE Software January l February 2002, pp 18–25.Google Scholar
  10. [Heimdahl 1996]
    Heimdahl M. and Leveson N. Completeness and consistency in hierachical state-based requirements. IEEE Transactions on Software Engineering SE-22, June 1996, pp 363–377.Google Scholar
  11. [Hodges 1992]
    Quoted in: Andrew Hodges. Alan Turing: The Enigma. Vintage, Random House, London, ISBN 0-09-911641-3 or Walker & Co., New York, ISBN 0-802-775802.Google Scholar
  12. [ITSEC 1991]
    Information Technology Security Evaluation Criteria (ITSEC). Provision Harmonised Criteria, Version 1. 2, June 1991.Google Scholar
  13. [Jackson 2001]
    See Scholar
  14. [Keller 1993]
    Keller T.W. Achieving error-jree man-rated software. 2nd international conference on Software Testing, Analysis and Review, Monterey, California, 1993.Google Scholar
  15. [King 2000]
    Steve King, Jonathan Hammond, Rod Chapman and Andy Pryor. Is Proof More Cost Effective Than Testing? IEEE Transactions on Software Engineering Vol 26, No 8, August 2000, pp 675–686CrossRefGoogle Scholar
  16. [Littlewood 1993]
    Littlewood, Bev; and Strigini, Lorenzo. Validation of Ultrahigh Dependability for Software-Based Systems. CACM 36 (11): 69–80 (1993)Google Scholar
  17. [MULTOS]
    See www.multos.eomGoogle Scholar
  18. [RTCA 1992]
    RTCA-EUROCAE. Software Considerations in Airborne Systems and Equipment Certification. DO-178BIED-12B. 1992.Google Scholar
  19. [Schubert 2003]
    Tom Schubert. ‘High Level Formal Verification of Next-Generation Microprocessors. Proceedings of 40th Design Automation Conference. ACM Press June 2003.Google Scholar
  20. [SPC 1993]
    Software Productivity Consortium. Consortium requirements engineering guidebook. Technical Report SPC-9206Q-CMC version 01.00.09.Google Scholar
  21. [Thomas 2003]
    Martyn Thomas. The Modest Software Engineer. Presention at Software Reliability and Metrics Club, London on 20th May 2003.Google Scholar
  22. [Warmer 2003]
    Jos Warmer. The future of UML. Scholar

Copyright information

© Springer-Verlag London 2004

Authors and Affiliations

  • Peter Amey
    • 1
  1. 1.Praxis Critical SystemsBathUK

Personalised recommendations