Logic versus Magic in Critical Systems

  • Peter Amey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2043)


A prevailing trend in software engineering is the use of tools which apparently simplify the problem to be solved. Often, however, this results in complexity being concealed or “magicked away”. For the most critical of systems, where a credible case for safety and integrity must be made prior to there being any service experience, we cannot tolerate concealed complexity and must be able to reason logically about the behaviour of the system. The paper draws on real-life project experience to identify some historical and current magics and their effect on high-integrity software development; this is contrasted with the cost and quality benefits that can be made from taking a more logical and disciplined approach.


Critical System Object Code Swap Operation Lifecycle Stage Aeronautical Engineering 
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.
    Dijkstra, Edsger: Go To Statement Considered Harmful. CACM Vol 11.No. 3 March 1968, pp 147–148.MathSciNetGoogle Scholar
  2. 2.
    RTCA-EUROCAE: Software Considerations in Airborne Systems and Equipment Certification. DO-178B/ED-12B. 1992.Google Scholar
  3. 3.
    Ives, Blake and Earl Michael: Mondex International: Reengineering Money. London Business School Case Study 97/2. See
  4. 4.
    Littlewood, Bev; and Strigini, Lorenzo: Validation of Ultrahigh Dependability for Software-Based Systems. CACM 36(11): 69–80 (1993)Google Scholar
  5. 5.
    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
  6. 6.
    Littlewood, B: Limits to evaluation of software dependability. In Software Reliability and Metrics (Procedings of Seventh Annual CSR Conference, Garmisch-Partenkirchen). N. Fenton and B. Littlewood. Eds. Elsevier, London, pp. 81–110.Google Scholar
  7. 8.
    Carré, Bernard: Reliable Programming in Standard Languages. In High-integrity Software. RSRE Malvern, Chris Sennett (Ed). ISBN 0-273-03158-9, 1989.Google Scholar
  8. 9.
    Amey, Peter: The INFORMED Design Method for SPARK. Praxis Critical Systems 1999.Google Scholar
  9. 10.
    Barnes, John: The SPARK Way to Correctness is Via Abstraction. ACM SIGAda 2000Google Scholar
  10. 11.
    Professor C.A.R. Hoare, The 1980 Turing award lecture. The Emperor’s Old Clothes. CACM Vol. 24.No.2 February 1981. pp 75–83Google Scholar
  11. 12.
    Finnie, Gavin et al: SPARK–The SPADE Ada Kernel. Edition 3.3, 1997, Praxis Critical SystemsGoogle Scholar
  12. 13.
    Finnie, Gavin et al: SPARK 95–The SPADE Ada 95 Kernel. 1999, Praxis Critical SystemsGoogle Scholar
  13. 14.
    Barnes, John: High Integrity Ada–the SPARK Approach. Addison Wesley Longman, ISBN 0-201-17517-7.Google Scholar
  14. 15.
    Sutton, James and Carré, Bernard: Ada, the Cheapest Way to Build a Line of Business”. 1994Google Scholar
  15. 16.
    Sutton, James and Carré, Bernard: Achieving High Integrity at Low Cost: A Constructive Approach. 1995Google Scholar
  16. 17.
    Croxford, Martin and Sutton, James: Breaking through the V&V Bottleneck. Lecture Notes in Computer Science Volume 1031, 1996.Google Scholar
  17. 18.
    Sutton, James: Cost-Effective Approaches to Satisfy Safety-critical Regulatory Requirements. Workshop Session, SIGAda 2000.Google Scholar
  18. 19.
    King, Hammond, Chapman and Pryor: Is Proof More Cost-Effective than Testing?. IEEE Transaction on Software Engineering, Vol. 26,No. 8, August 2000, pp 675–686.CrossRefGoogle Scholar
  19. 20.
    Bergeretti and Carré: Information-flow and data-flow analysis of while-programs. ACM Transactions on Programming Languages and Systems 1985.Google Scholar
  20. 21.
    Santhanam, Viswa; Wright, Peggy A.; Decker-Lindsey, Barbara: Dataflow Coverage in the Boeing 777 Primary Flight Control Software. Boeing 1995Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

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

Personalised recommendations