Colin Snook

Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on the expertise and experience of human intervention to make critical judgements. While human judgement is essential to an analysis method, it is also important to ensure a degree of formality so that we reason about safety and security at early stages of analysis and design, rather than detect problems later. In this paper, we present a hierarchical and incremental analysis process that aims to justify the design and flow-down of derived critical requirements arising from safety hazards and security vulnerabilities identified at the system level. The safety and security analysis at each level uses STPA-style action analysis to identify hazards and vulnerabilities. At each level, we verify that the design achieves the safety or security requirements by backing the analysis with formal modelling and proof using Event-B refinement. The formal model helps to identify hazards/vulnerabilities arising from the design and how they relate to the safety accidents/security losses being considered at this level. We then re-apply the same process to each component of the design in a hierarchical manner. Thus, we use hazard and vulnerability analysis, together with refinement-based formal modelling and verification, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical system-level requirements down to component-level requirements, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards/vulnerabilities are mitigated.