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.

SUMMARY This paper is concerned with the correct specification and validation of quality attribute requirements (QARs) that crosscut through a diverse set of complex system functions. These requirements act as modifiers of system level functional requirements and thus have substantial influence on the eventual architectural selection. Because system designers traditionally address these requirements one quality attribute at a time, the process frequently results in QARs that contain subtle conflicting behaviors. This paper presents an approach to QAR‐induced behavior validation and conflict detection via execution‐based model checking early in the software development process. It explores the concept of conflicts between requirements with temporal and sequencing behaviors and presents an automated approach for discovering such conflicts. Published 2012. This article is a US Government work and is in the public domain in the USA.

Studies have suggested that formal specifications and lightweight formal methods help improve the clarity and precision of the requirements specification. This paper describes a process to augment the current informal approaches to system-of-systems development by introducing temporal assertions to capture the safety-critical and mission-essential system requirements and runtime model checking to evaluate the system designs and implementation. The process allows users to develop and validate temporal assertions iteratively via simulation with multiple scenarios, and to use the assertions to automate the testing of the system-of-systems under development as well as armor-plating the target system against any unexpected behaviors at runtime.

Summary form only given. This paper describes TLCharts, a visual specification language that combines the visual and intuitive appeal of nondeterministic Harel statecharts with formal specifications written in linear-time (metric) temporal logic (LTL and MTL). The formalism is described using a practical infusion pump requirement example. The infusion pump TLChart specification is then compared with two competing representations: temporal logic and deterministic Harel statecharts. The infusion pump example is also used to point out the strength of each constituent TLCharts component. We provide an informal semantics for TLCharts using nondeterministic automata with negation and overlapping states. Finally, we show how natural language snippets are used instead of TLChart temporal logic conditions thereby inducing a formalism we call NTLCharts.

Run-time monitoring is a lightweight verification method whereby the correctness of a programs' execution is verified at run-time using executable specifications. This paper describes the verification of the fault protection engine of the Deep-Impact spacecraft flight software using a temporal logic based run-time monitoring tool.

We investigate the descriptive succinctness of three fundamental notions for modeling concurrency: nondeterminism and pure parallelism, the two facets of alternation, and bounded cooperative concurrency , whereby a system configuration consists of a bounded number of cooperating states. Our results are couched in the general framework of finite-state automata, but hold for appropriate versions of most concurrent models of computation, such as Petri nets, statecharts or finite-state versions of concurrent programming languages. We exhibit exhaustive sets of upper and lower bounds on the relative succinctness of these features over Σ * and Σ ω , establishing that: For example, we prove exponential upper and lower bounds on the simulation of deterministic concurrent automata by AFAs, and triple-exponential bounds on the simulation of alternating concurrent automata by DFAs.

The authors presents a simple, single-block implementation scheme for state charts which uses a single conventional combinational-logic block and a state register. The most attractive feature of the proposed scheme is the absence of communication. It eliminates the need for communicating FSMs (finite state machines) owing to an older realization method, and does so without having to account for all state configurations implied by concurrency. The author investigates the state encoding conditions for the implementation and suggests an appropriate optimization technique.>

Given a system of n interacting finite state machines (FSMs) and a state configuration, the reachability problem is to examine whether this configuration is reachable within the system. An investigation is made of the complexity of this decision problem and three of its derivatives, namely, (1) verifying system determination, (2) testing for the existence of unspecified inputs to any FSM within the system, and (3) testing for exclusiveness of two intra-FSM signals. It is proved that these problems are all PSPACE-complete. The effect of these problems on the state assignment process for concurrent systems of interacting FSMs is also shown.>

Currently, symbolic cover minimization is computed using multiple-valued-logic minimization. This problem, however, is computationally intractable, so less accurate heuristics are used. An alternative approach to computationally intractable problems is to reduce their generality so that the simpler problem has a tractable solution. Accordingly, a deterministic approach for the symbolic cover minimization problem for fully input/output (I/O) specified finite state machines (FSMs) is presented. A uniqueness theorem for a hierarchical extension of FSMs is proved, and the theorem is used to derive the proposed technique.>

Statecharts have been proposed recently as a visual formalism for the behavioral description of complex systems. They extend classical state diagrams in several ways, while retaining their formality and visual nature. The authors argue that statecharts can be beneficially used as a behavioral hardware description language. They illustrate some of the main features of the approach, including: hierarchical decomposition, multilevel timing specifications and flexible concurrency and synchronization capabilities. The authors also present a VLSI synthesis methodology by which layer area and delay periods can be reduced relative to the conventional finite-state-machine (FSM) synthesis method.>