Implementability of requirements in the four-variable model

• We study implementability of system requirements in the general, relational four-variable model.
• We formalize a demonic acceptability criterion for safety-critical software.
• We prove a necessary and sufficient existence condition for acceptable software.
• This condition allows for implementability checks early in system development.
• The condition is also useful in determining the tolerances needed on unimplementable system requirements.

Many safety-critical computer systems are required to monitor and control physical processes. The four-variable model, which has been used successfully in industry for almost four decades, helps to clarify the behaviors of, and the boundaries between the physical processes, input/output devices, and software. In this model, the acceptable behaviors of the software are constrained by the physical environment, system requirements, and input/output devices. If acceptable software behaviors are possible, then the system requirements are said to be implementable with respect to these constraints. The only acceptability condition proposed in the literature deems as acceptable software behaviors that can lead to undesirable system behaviors, in particular, nondeterministic system behaviors that for the same input sometimes do not produce any results and some other times produce expected results. In this sense, the acceptability condition can be seen as angelic. In this paper we strengthen the acceptability condition using the demonic calculus of relations such that no undesirable system or software behaviors are allowed and prove a necessary and sufficient implementability condition for the system requirements. As a byproduct, we also obtain a mathematical characterization of the least restrictive software specification, which, for all intents and purposes, can play the role of the software requirements.