Use of Statechart Assertions for Modeling Human-in-the-Loop Security Analysis and Decision-Making Processes.

摘要

Processes are a fundamental component of most activities undertaken by humans. In software engineering and information assurance, in particular, it is important that processes be understandable, documented, and repeatable so as to ensure that the process outcomes are consistent and predictable. This dissertation provides a novel approach to process creation, documentation, checking, and maintenance that applies mathematical formalism to the engineering of processes that rely in large measure on human decision-making to advance the process flow. However, the modeling approach is sufficiently general for application to any process. This dissertation advances the state-of- the-art in software engineering by providing a formal computer-assisted end-to- end way to conduct requirements engineering. This dissertation advances the state-of-the-art in information assurance by developing a systematic approach that makes the creation of security processes precise and uses formal methods to allow upfront validation and runtime verification of modeled processes. This dissertation demonstrates the modeling approach through a case study of the Unified Cross Domain Management Office's Cross Domain Solution Workflow process.