Implementability of Requirements for Safety-Critical Embedded Systems
Theses
Overview
Overview
abstract
Computer systems are used for controlling physical processes in many safety-critical applications. These systems are embedded into the larger system of the application and are interfaced with their physical environment using input hardware (sensors, analog-to-digital converters) and output hardware (digital to analog converters, actuators). A challenging task in designing such systems is finding the right combination of input hardware, output hardware, and software such that their integration produces systems that satisfy their requirements.
In this thesis we propose a mathematical basis for checking, without the need for developing and verifying a detailed implementation, if acceptable soft- ware exists given the chosen hardware interfaces. The requirements framework we use is the relational four-variable model proposed by Parnas and Madey. This model helps to clarify the behaviour of, and the boundaries between, the system’s physical environment, hardware interfaces, and software, which are all described as input-output relations without detail about internal state.
The semantics of the four-variable model proposed by Parnas and Madey, which may be seen in relation algebraic terms as an angelic semantics, allows system descriptions that are not completely consistent with the natural laws of the physical environment. To address this issue, we redefine in the demonic calculus of relations the notion of feasibility of system requirements proposed by Parnas and Madey such that the system requirements specify for every input possible in the environment only behaviours allowed by the environment. We also redefine in the demonic calculus of relations the system and software acceptability criterion of Parnas and Madey to reject nonterminating or empty implementations, and prove a necessary and sufficient existence condition for
acceptable software. This condition has a constructive flavour and yields the weakest (least restrictive, or least refined) specification of the software requirements.
A practical implication of the necessary and sufficient condition is that in a relational four-variable model, as opposed to the functional case, the input and output hardware interfaces are mutually dependent and changes to either may require changes to the other. We prove two stronger conditions that allow the decoupling of the hardware interfaces while still guaranteeing the ability of the software to meet the system requirements.
For the cases when the system requirements are feasible, but an accept- able implementation does not exist, a typical engineering approach is to relax the requirements by allowing tolerances. We show how the necessary and sufficient condition can be used in the derivation of tolerances on the requirements for a pressure sensor trip in the shutdown system of a nuclear reactor such that the requirements become implementable.
