Iterative Analysis to Improve Key Properties of Critical Human-Intensive Processes: An Election Security Example

摘要: In this article, we present an approach for systematically improving complex processes, especially those involving human agents, hardware devices, and software systems. We illustrate the utility of by applying it to part election process show how can improve security correctness that subprocess. use Little-JIL definition language create a precise detailed process. Given definition, two forms automated analysis explore whether specified key properties, such as safety policies, be undermined. First, model checking identify execution sequences fail conform event-sequence properties. After these are addressed, apply fault tree when misperformance steps might allow undesirable outcomes, breaches. The results analyses provide assurance about process; suggest areas improvement; and, applied modified evaluate proposed changes.