Practical application of functional and relational methods for the specification and verification of safety critical software

by M. Lawford, J. McDougall, P. Froebel and G. Moum

Abstract: 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.

Download

PDF (214k)

Download (via Springer) - nice hyperlinked PDF

PDF

BibTeX Entry

@InProceedings{LMFM00,
  author =       {M. Lawford and J. McDougall and P. Froebel and
                  G. Moum},
  title =        {Practical application of functional and relational
                  methods for the specification and verification of
                  safety critical software},
  booktitle =    "Proceedings Algebraic Methodology and Software
                  Technology, 8th International Conference, AMAST
                  2000, Iowa City, Iowa, USA, May 2000",
  year =         2000,
  editor =       "T. Rus",
  volume =       1816,
  series =       "LNCS",
  pages =        "73--88",
  publisher =    "Springer",
  key =          "LMFM00"
}