Three Perspectives in Formal Engineering

  • John McDermid
  • Andy Galloway
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


We present three perspectives of the use of formalism in the construction of High-Integrity Embedded Real-time Systems. In the first, we describe the long-term research aims. The scope is the entire system, the goal is to demonstrate intentional correctness, and the emphasis is on scientific certainty. In the second, we present medium-term research aims. The scope is more on the software in the system, and the emphasis shifts to the notion of engineering confidence. Following on from the medium-term view we propose a set of challenges for formal engineering methods research, based on our perception of the technical issues surrounding the provision of viable engineering solutions. In the third perspective we discuss the short term. In particular, we describe how our recent research is attempting to meet some of the proposed challenges, as a first step towards our medium and long-term aspirations.


Embed System Proof Obligation Monitor Variable Problem Frame Formal Engineer 
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.
    McDermid, J., Galloway, A., et al.: Towards Industrially Applicable Formal Methods: Three Small Steps, and One Giant Leap. In: Proceedings of International Conference on Formal Engineering Methods (ICFEM) 1998. IEEE Press, Los Alamitos (1998)Google Scholar
  2. 2.
    Parnas, D., Madey, J.: Functional Documents for Computer Programs. Science of Computer Programming 25(1) (1995)Google Scholar
  3. 3.
    UK Ministry of Defence, Defence Standard 00-56 Issue 2: Safety Management Requirements for Defence Systems (1996)Google Scholar
  4. 4.
    Australian Department of Defence, Australian Defence Standard Def(Aust) 5679: Procurement of Computer-based Safety Critical Systems (1998)Google Scholar
  5. 5.
    German, A.: Software Static Code Analysis, Lessons Learned. Crosstalk (November 2003)Google Scholar
  6. 6.
    King, S., Hammond, J., Chapman, R., Pryor, A.: Is Proof more Cost-Effective than Tesing? IEEE Transactions on Software Engineering 26(8) (2000)Google Scholar
  7. 7.
    Galloway, A., Iwu, F., McDermid, J., Toyn, I.: On the Formal Development of Safety-Critical Software. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 362–373. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Jackson, M.A.: Problem Frames. Addison-Wesley, Reading (2001)Google Scholar
  9. 9.
    Rapanotti, L., Hall, J.G., Jackson, M.A., Nuseibeh, B.: Architecture-driven Problem Decomposition. In: Proceedings of RE 2004. IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  10. 10.
    Airline Electronic Engineering Committee, ARINC, Supplement 1 to ARINC Specification 653: Avionics Application Software Standard Interface, Standard 03-116/SWM-89, Annapolis Maryland (2003)Google Scholar
  11. 11.
    Stepney, S., Polack, F., Toyn, I.: Patterns to Guide Practical Refactoring: examples targetting promotion in Z. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 20–39. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Paige, R.F., Chivers, H., McDermid, J.A., Stephenson, Z.R.: High Integrity Extreme Programming. In: Symposium on Applied Computing. ACM, New York (2005)Google Scholar
  13. 13.
    Galloway, A.J., Cockram, T.J., McDermid, J.A.: Experiences with the Application of Discrete Formal Methods to the Development of Engine Control Software. In: Proceedings of Distributed Computer Control Systems DCCS 1998. IFAC - International Federation of Automatic Control (1998)Google Scholar
  14. 14.
    Iwu, F., Galloway, A., Toyn, I., McDermid, J.A.: Practical Formal Specification For Embedded Control Systems. In: Proceedings of the 11th IFAC Symposium on Information Control Problems in Manufacturing, INCOM 2004, Salvador, Brazil, April 5-7 (2004)Google Scholar
  15. 15.
    Toyn, I., Galloway, A.: Proving Properties of Stateflow Models using ISO Standard Z and CADiZ. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 104–123. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Arthan, R., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: Control Laws. In: Liu, S., McDermid, J.A., Hinchey, M.G. (eds.) Proceedings of ICFEM 2000. IEEE Computer Society, Los Alamitos (2000)Google Scholar
  17. 17.
    Galloway, A., Blow, J.: Multilayered Domain Specific Formal Methods. In: Proceedings of The Joint Workshop on Formal Specification of Computer Based Systems, Washington DC, University of Stirling (April 2001)Google Scholar
  18. 18.
    Blow, J., Galloway, A.: Generalised Substitution Language and Differentials. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 396. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    Blow, J.R.: Use of Formal Methods in the Development of Safety-critical Control Software. DPhil thesis, Department of Computer Science, University of York. YCST-2003-08 (2003)Google Scholar
  20. 20.
    Poppleton, M., Banach, R.: Retrenchment, Refinement and Simulation. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, p. 304. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  21. 21.
    Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138 (1995)Google Scholar
  22. 22.
    Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  23. 23.
    Atiya, D.M.: On extending the SPARK toolset for reasoning about floating point arithmetic: II. Technical Report, UTC, Department of Computer Science, University of York. YUTC/TR/2005/06 (See also YUTC/TR/2005/01) (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • John McDermid
    • 1
  • Andy Galloway
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkHeslington, YorkUK

Personalised recommendations