A Rigorous Analysis of the Safety and Security in Cyber-Physical Systems

The conflict among dependability properties, such as safety and security in cyber-physical systems, requires a coanalysis of both aspects to ensure the dependability of such systems. Therefore, it is important to employ integrated method-ologies for analysing safety and security to mitigate design flaws. Traditional safety analysis approaches, focusing on component failures and simple cause-and-effect chains, cannot find unsafe events caused by complex system interconnections. On the other hand, Systems Theoretic Process Analysis (STPA) considers losses to be the result of interactions but does not leverage threat models to find potential security and their effects on system safety. In this work, our approach integrates both systematic analysis (STPA and STRIDE) and formal methods (Event-B) to address both safety and security concerns and apply suitable design constraints. Also, implementing Event-B formalism helps us to rigorously specify the safety and security constraints and verify the system's behaviour. We apply our approach to an emergency vehicular system to demonstrate its effectiveness.