Precise Documentation and Validation of Requirements

Abstract

Precise documentation of requirements is important for developing and certifying mission critical software. We specify cyber-physical systems via an Event-B-like machine which declar es the monitored and controlled variables and their initial condition. A machine event models the joint action of the plant and the controller. Embedded in the event action is a function table that specifies the input-output behaviour of the controller, as monitored variables are periodically updated by the plant. We extend the Event-B notation with queries and modules. The resulting machine provides us with a mathematical description of the overall system behaviour, thus allowing us to validate the requirements by proving that (1) the input-output specification of the controller is complete, disjoint and well-defined, and that (2) the machine satisfies system-wide consistency invariants elicited from domain experts. A biomedical device is used as a case study, and we mechanize proofs via a SMT solver. © Springer International Publishing Switzerland 2014.