Practical Application of Functional and Relational Methods for the Specification and Verification of Safety Critical Software

  • Mark Lawford
  • Jeff McDougall
  • Peter Froebel
  • Greg Moum
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


In this paper we describe how a functional version of the 4-variable model can be decomposed to improve its practical application to industrial software verification problems. An example is then used to illustrate the limitations of the functional model and motivate a modest extension of the 4-variable model to an 8-variable relational model. The 8-variable model is designed to allow the system requirements to be specified as functions with input and output tolerance relations, as is typically done in practice. The goal is to create a relational method of specification and verification that models engineering intuition and hence is easy to use and understand.


Finite State Machine Relational Method Variable Accuracy Proof Obligation Monitor Variable 
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.
    R. Janicki and R. Khédri. On a formal semantics of tabular expressions. Science of Computer Programming, 2000. To appear.Google Scholar
  2. 2.
    R. Janicki, D. Parnas, and J. Zucker. Tabular representations in relational documents. In C. Brink et al., editors, Relational Methods in Computer Science, Advances in Computing Science, ch. 12, p. 184–196. Springer Wien New York, 1997.Google Scholar
  3. 3.
    E. Jankowski and J. McDougall. Procedure for the Specification of Software Requirements for Safety Critical Software. CANDU Computer Systems Engineering Centre of Excellence Procedure CE-1001-PROC Rev. 1, July 1995.Google Scholar
  4. 4.
    P. Joannou et al. Standard for Software Engineering of Safety Critical Software. CANDU Computer Systems Engineering Centre of Excellence Standard CE-1001-STD Rev. 1, January 1995.Google Scholar
  5. 5.
    M. Lawford and P. Froebel. Application of tabular methods to the specification and verification of a nuclear reactor shutdown system. Submitted to FMSD.Google Scholar
  6. 6.
    J. McDougall and J. Lee. Procedure for the Software Design Description for Safety Critical Software. CANDU Computer Systems Engineering Centre of Excellence Procedure CE-1002-PROC Rev. 1, October 1995.Google Scholar
  7. 7.
    J. McDougall, M. Viola, and G. Moum. Tabular representation of mathematical functions for the specification and verification of safety critical software. In SAFE-COMP’94, p. 21–30, Anaheim, October 1994. Instrument Society of America.Google Scholar
  8. 8.
    G. Moum. Procedure for the Systematic Design Verification of Safety Critical Software. CANDU Computer Systems Engineering Centre of Excellence Procedure CE-1003-PROC Rev. 1, December 1997.Google Scholar
  9. 9.
    Sam Owre, John Rushby, and N. Shankar. Integration in PVS: Tables, types, and model checking. In Ed Brinksma, editor, TACAS’ 97, LNCS 1217, p. 366–383, Enschede, The Netherlands, April 1997. Springer-Verlag.Google Scholar
  10. 10.
    D. Parnas. Tabular representation of relations. Technical Report 260, Communications Research Laboratory, McMaster University, October 1992.Google Scholar
  11. 11.
    D. Parnas and J. Madey. Functional documentation for computer systems engineering. Technical Report CRL No. 273, Telecommunications Research Institute of Ontario, McMaster University, September 1991.Google Scholar
  12. 12.
    N. Shankar, S. Owre, and J. M. Rushby. PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Mark Lawford
    • 1
  • Jeff McDougall
    • 2
  • Peter Froebel
    • 3
  • Greg Moum
    • 3
  1. 1.Computing and SoftwareMcMaster Univ.HamiltonCanada
  2. 2.JKM Software Technologies Inc.Kettleby
  3. 3.Ontario Power GenerationTorontoCanada

Personalised recommendations