Resiliency Analysis of Mission-Critical System of Systems Using Formal Methods

A System of Systems (SoS) is a formation of heterogeneous systems that work together effectively to accomplish critical missions. These mission-critical SoS ensure the safety and security of any nation. Attacks on mission-critical SoS can have devastating outcomes. We need to design missions that are resilient to attacks. SoS engineering must specify, analyze, and understand where adverse events are possible and how to mitigate them while a mission-critical SoS is deployed. This work uses an end-to-end methodology for analyzing the resiliency of mission-critical SoS. The methodology starts with representing SoS mission as a workflow. It then converts the workflow into formal representation using Coloured Petri Nets (CPN). Threat models are extracted from the mission specification, which are used to construct the CPN representations of the attacks. The mission specifications and the attacks are composed to analyze the mission resiliency. The analysis identifies if the mission succeeds, fails, and is incomplete. We apply the methodology to an SoS consisting of a military vehicle and route-reconnaissance drones working together to monitor a national border and respond immediately to any physical threats. The result demonstrates how to restrict the mission to improve the resiliency of SoS formation. Such methodology is important for the early design stage of resilient mission-critical SoS.