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.