Modeling Human-in-the-Loop Security Analysis and Decision-Making Processes

doi:10.1109/TSE.2014.2302433

2014-02-01

PRE

Michael A. Schumann *

Doron Drusinsky

James Michael

Duminda Wijesekera

DOI：10.1109/TSE.2014.2302433

原文链接

原文求助

摘要

En 中文

This paper presents a novel application of computer-assisted formal methods for systematically specifying, documenting, statically and dynamically checking, and maintaining human-centered workflow processes. This approach provides for end-to-end verification and validation of process workflows, which is needed for process workflows that are intended for use in developing and maintaining high-integrity systems. We demonstrate the technical feasibility of our approach by applying it on the development of the US government's process workflow for implementing, certifying, and accrediting cross-domain computer security solutions. Our approach involves identifying human-in-the-loop decision points in the process activities and then modeling these via statechart assertions. We developed techniques to specify and enforce workflow hierarchies, which was a challenge due to the existence of concurrent activities within complex workflow processes. Some of the key advantages of our approach are: it results in development of a model that is executable, supporting both upfront and runtime checking of process-workflow requirements; aids comprehension and communication among stakeholders and process engineers; and provides for incorporating accountability and risk management into the engineering of process workflows.

Keyword:

Formal methods

information assurance

process modeling

software engineering

statechart assertions

verification and validation