Modelling and Verification of Survivability Requirements for Critical Systems

Survivability is a property of systems that guarantees services which operate safe and timely. Safety-critical services must survive despite the presence of faults or attacks. The contribution of the paper is twofold: construction of a survivability assessment model (SAM) and its transformation to a model checking problem. Our SAM is automatically obtained from an improved specification of misuse cases, which encompasses essential services, threats and survivability strategies. The SAM is automatically converted, using model-driven techniques, into a Petri Net model for verifying survivability properties through model checking. The method has been applied to a military command-and-control information system.