Question 6 of 9: Critical Software Development

Question 6: Critical Software Development (20 marks)

Question text not reproduced: the examination questions are © Engineers and Geoscientists BC. Open the official past paper (linked at the top of this page) to read the question, then follow the worked solution below.

(a) Three Complementary Approaches to Dependability

Fault avoidance aims to prevent faults from ever being introduced into the software in the first place, through disciplined development processes, rigorous or formal specification, and design practices that minimize opportunities for error. Fault detection and removal accepts that some faults will still slip through avoidance and uses verification and validation activities — testing, code inspection, static analysis, formal verification — to find and eliminate them before the system is delivered. Fault tolerance accepts that some faults will still remain even after detection efforts and designs the running system to keep operating correctly, or at least fail safely, in their presence — through redundancy, exception handling, and graceful degradation. The three are complementary rather than alternatives: avoidance reduces how many faults are ever introduced, detection removes most of what avoidance failed to prevent, and tolerance is the last line of defence against the small residue that inevitably survives both earlier stages, which is unavoidable in any system of realistic size and criticality.

(b) Four Techniques for Fault-Free Software

1. Formal specification and verification. Writing the requirement or a critical algorithm in a mathematically precise notation (e.g. Z or VDM) removes the ambiguity of natural language, and formally proving the implementation satisfies that specification can eliminate whole classes of logic error before any code is run. 2. Static analysis under a restricted, disciplined coding style. Automated tools examine the source code without executing it, flagging constructs known to cause faults (uninitialized variables, out-of-bounds array access, unreachable code); their effectiveness is greatly increased by restricting the language subset used (structured control flow, no unconstrained pointer arithmetic) so the analysis can reason about the code exhaustively rather than approximately. 3. Systematic peer inspection (Fagan-style inspections/walkthroughs). A structured group review of a design or code artifact, conducted before testing even begins, catches classes of defect (misunderstood requirements, subtle logic errors) that automated testing is poor at finding and does so at a fraction of the cost of finding the same defect later via failure in the field. 4. Reuse of pre-verified, trusted components under design-by-contract. Building new functionality from libraries or components that have already been extensively verified and that publish an explicit contract (preconditions the caller must satisfy, postconditions the component guarantees) avoids re-introducing faults into code that has, in effect, already been debugged by prior use, and the contract makes any misuse of the component an easily detectable violation rather than a silent defect.

(c) Applying the Techniques to a Software-Controlled Insulin Pump

Because a dosing error can directly endanger the patient's life, all four techniques are applied deliberately to this specific system. Formal specification is used on the dosing algorithm itself: the relationship between the sensed blood-sugar-proportional signal and the commanded insulin dose is written as a precise mathematical function with proven bounds, so that it can be shown, for the full plausible range of sensor readings, that the computed dose can never exceed a safe maximum — this is the single highest-value place to invest formal methods, since it is the one calculation that most directly determines patient safety. Static analysis under a restricted coding subset (an embedded-safety style discipline, analogous to MISRA C) is applied to the control-loop firmware, banning dynamic memory allocation, unbounded recursion, and other constructs that could cause an unpredictable runtime failure in code that must never simply crash mid-dose. Independent inspection of the sensor-fusion and dosing-decision logic by engineers who did not write it is used specifically because realistic physiological fault conditions (a failing sensor drifting slowly out of calibration, a partially occluded needle) are difficult and unsafe to reproduce in an automated test rig, so a careful human review of how the logic behaves under each conceivable sensor-failure mode substitutes for tests that cannot ethically be run on a live patient. Reuse of pre-verified, contracted components means the pump-actuator driver and the real-time scheduling kernel are taken from an already-certified medical-device library rather than written fresh, so the newly written code is confined to the smallest possible surface area (the dosing decision itself) that has not already been independently verified. Finally, because even these four techniques cannot guarantee zero residual faults, fault tolerance is layered underneath all of them: dual redundant blood-parameter sensors are cross-checked by majority vote before any dose is computed, an independent hardware watchdog cuts power to the pump actuator if the control loop fails to complete within its deadline, and a hard maximum-dose limit is enforced by simple, separately verified hardware logic that the main control software cannot override — so that a single software fault, should one still exist despite the four techniques above, cannot by itself cause an overdose.