Lecture Notes in Computer Science, 2000, Volume 1816/2000, 73-88, DOI: 10.1007/3-540-45499-3_8

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

Mark Lawford, Jeff McDougall, Peter Froebel and Greg Moum

View Related Documents

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.
Partially supported by NSERC grant 217249-99.

Fulltext Preview

Image of the first page of the fulltext document