Modelling and analysing Defence-in-Depth in arming systems

Safety analysis of high consequence arming systems is complex, many arguments about the behaviour of a design are required to validate that the system fulfils its safety requirements. Manual analysis of such systems can miss potential paths of energy flow and this process becomes increasingly difficult when the concept of defence in depth is incorporated into the design. Utilising the process algebra Communicating Sequential Processes allows component specifications and system level safety specifications to be formalised. Model checking techniques can then be applied to ensure the design of each component meets their individual specifications and that when composed together achieve the required system level behaviour, demonstrating both system level safety and meeting the requirements of defence in depth. We present validation of the technique through the use of a small example representative of the systems of interest we are analysing. The approach is then demonstrated to identify potential problems in this example through various scenarios.