A model-driven approach to survivability requirement assessment for critical systems. (October 2016)

• Record Type: Journal Article
• Authors: Bernardi, Simona; Dranca, Lacramioara; Merseguer, José
• Other Names: Nowakowski Tomasz guest-editor.; Zio Enrico guest-editor.
• Is Part Of: Proceedings of the Institution of Mechanical Engineers. Volume 230:Number 5(2016:Oct.)
• Page Start: 485
• Page End: 501
• Publication Date: 2016-10
• Subjects: Misuse cases -- UML profiling -- Petri net -- model checking -- survivability -- model-to-model and model-to-text transformations; Reliability (Engineering) -- Mathematical models -- Periodiclals; Risk assessment -- Mathematical models -- Periodicals; Engineering design -- Mathematical models -- Periodicals; 620.00452
• DOI: 10.1177/1748006X15626017
• Languages: English
• ISSNs: 1748-006X

Abstract

Survivability is a crucial property for those systems – such as critical infrastructures or military Command and Control Information Systems – that provide essential services, since the latter must be operational even when the system is compromised due to attack or faults. This article proposes a model-driven method and a tool – MASDES – to assess the survivability requirements of critical systems. The method exploits the use of (1) (mis)use case technique and UML profiling for the specification of the survivability requirements and (2) Petri nets and model checking techniques for the requirement assessment. A survivability assessment model is obtained from an improved specification of misuse cases, which encompasses essential services, threats and survivability strategies. The survivability assessment model is then converted into a Petri net model for verifying survivability properties through model checking. The MASDES tool has been developed within the Eclipse workbench and relies on Papyrus tool for UML. It consists of a set of plug-ins that enable (1) to create a survivability system view using UML and profiling techniques and (2) to verify survivability properties. In particular, the tool performs model transformations in two steps. First, a model-to-model transformation generates, from the survivability view, a Petri net model and properties to be checked in a tool-independent format. Second, model-to-text transformations produce the Petri net specifications for the model checkers. A military Command and Control Information Systems has been used as a case study to apply the method and to evaluate the MASDES tool, within an iterative-incremental software development process.