This article presents a static deadlock analysis for single-path MPI programs. Deadlock is when processes are blocked indefinitely by a circular communication dependency. A single path program is one that does not decode messages for control flow. The analysis records a program execution in the form of a trace and then determines from that trace whether there exists any feasible deadlocking schedules. The primary contribution is the combining of identical consecutive sends or receives into single macro actions. This simplified trace is analyzed for potential deadlock cycles. An abstract machine identifies infeasible cycles, and those not identified by the machine are encoded as satisfiability problems for an SMT solver to resolve. The action combination reduces the complexity of identifying and filtering cycles before needing the costly SMT solver. This article shows the effectiveness of the action combination in experiments on a benchmark suite comparing to traces without action combination and other state-of-the-art deadlock analyses.

Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they either gracefully recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program is developing tools for design, analysis, and verification that enable systems engineers to design-in cyber-resiliency in a Model-Based Systems Engineering environment. This paper describes automated model transformations that introduce high-assurance cyber-resiliency components into a system, in particular filters and monitors that prevent malicious input and detect supply chain attacks, respectively. A formal specification defines each high-assurance component, and is used to verify that the component addresses system level cyber requirements. Implementations for these high-assurance components are directly synthesized from their specifications, and are automatically proven to preserve the exact meaning of the specifications all the way down to the binary code level. The model transformations are integrated into the Open Source AADL Tool Environment (OSATE). The paper further reports on a case study applying security-enhancing model transformations to a UAV system that uses the Air Force Research Laboratory's OpenUxAS services for route planning. In the case study, the model transformations add filters to guard against malformed input, as well as monitors to guard against ground station spoofing and malicious flight plans from OpenUxAS.

A common problem in MPI programs is deadlock: when two or more processes are blocked indefinitely due to a circular communication dependency. Automatically detecting deadlock is difficult due to its schedule-dependent nature. This paper presents a predictive analysis for single-path MPI programs that observes a single program execution and then determines whether any other feasible schedule of the program can lead to a deadlock. The analysis works by identifying problematic communication patterns in a dependency graph to form a set of deadlock candidates. The deadlock candidates are filtered by an abstract machine and ultimately tested for reachability by an SMT solver with an efficient encoding for deadlock. This approach quickly yields a set of high probability deadlock candidates useful for reasoning about complex codes and yields higher performance overall in many cases compared to other state-of-the-art analyses. The analysis is sound and complete for single-path MPI programs on a given input.

Task parallel programming models such as Habanero Java help developers write idiomatic parallel programs and avoid common errors. Data race freedom is a desirable property for task parallel programs but is difficult to prove because every possible execution of the program must be considered. A partial order over events of an observed program execution induces an equivalence class of executions that the program may also produce. The Does-not-Commute (DC) relation is an efficiently computable partial order used for data race detection. As a relatively weak partial order, the DC relation can represent relatively large equivalence classes of program executions. However, some of these executions may be infeasible, thus leading to false data race reports. The contribution of this paper is a mechanized proof that the DC relation is actually sound for commonly used task parallel programming models. Sound means that the first data race identified by the DC relation is guaranteed to be a real data race. A prototype analysis in the Java Pathfinder model checker shows that the DC relation can significantly reduce the number of explored states required to prove data race freedom in Habanero Java programs. In this application, the search for data race using the DC relation is both sound and complete.

Animals such as bees, ants, birds, fish, and others are able to perform complex coordinated tasks like foraging, nest-selection, flocking and escaping predators efficiently without centralized control or coordination. Conventionally, mimicking these behaviors with robots requires researchers to study actual behaviors, derive mathematical models, and implement these models as algorithms. We propose a distributed algorithm, Grammatical Evolution algorithm for Evolution of Swarm bEhaviors (GEESE), which uses genetic methods to generate collective behaviors for robot swarms. GEESE uses grammatical evolution to evolve a primitive set of human-provided rules into productive individual behaviors. The GEESE algorithm is evaluated in two different ways. First, GEESE is compared to state-of-the-art genetic algorithms on the canonical Santa Fe Trail problem. Results show that GEESE outperforms the state-of-the-art by (a) providing better solution quality given sufficient population size while (b) utilizing fewer evolutionary steps. Second, GEESE outperforms both a hand-coded and a Grammatical Evolution-generated solution on a collective swarm foraging task.

In this work, we propose the use of multi-agent system (MAS) models as the basis for predictive reasoning about various safety conditions and the performance of Air Traffic Management (ATM) Systems. To this end, we describe the engineering of a domain-specific MAS model that provides constructs for creating scenarios related to ATM systems and procedures; we then instantiate the constructs in the ATM model for different scenarios. As a case study we generate a model for a concept that provides the ability to maximize departure throughput at La Guardia airport (LGA) without impacting the flow of the arrival traffic; the model consists of approximately 1.5 hours real time flight data. During this time, between 130 and 150 airplanes are managed by four en-route controllers, three TRACON controllers, and one tower controller at LGA who is responsible for departures and arrivals. The planes are landing at approximately 36 to 40 planes an hour. A key contribution of this work is that the model can be extended to various air-traffic management scenarios and can serve as a template for engineering large-scale models in other domains.

The papers in this special section focus on systematic approaches to human-machine interface applications. The motivation for this special issue is the growing increase of remote mission management, unmanned aircraft systems, NextGen operations in the U.S. and its Single European Sky Air Traffic Management Research counterparts in Europe, and other similarly integrated systems of systems that include complex human–machine systems with high levels of autonomy and team dynamics that are difficult to understand and analyze. The issue explores key research areas that impact the properties of these systems, which rely on varied degrees of human and machine interactions. The special issue is a result of the continued interest in the formal verification of complex human–machine systems.

Habanero is a task parallel programming model that provides correctness guarantees to the programmer. Even so, programs may contain data races that lead to non-determinism, which complicates debugging and verification. This paper presents a sound algorithm based on permission regions to prove data race and deadlock freedom in Habanero programs. Permission regions are user annotations to indicate the use of shared variables over spans of code. The verification algorithm restricts scheduling to permission region boundaries and isolation to reduce verification cost. The effectiveness of the algorithm is shown in benchmarks with an implementation in the Java Pathfinder (JPF) model checker. The implementation uses a verification specific library for Habanero that is tested using JPF for correctness. The results show significant reductions in cost, where cost is controlled with the size of the permission regions, at the risk of rejecting programs that are actually free of any data race or deadlock.

Asynchronous message passing is an important paradigm in writing applications for embedded heterogeneous multicore systems. The Multicore Association (MCA), an industry consortium promoting multicore technology, is working to standardize message passing into a single API, MCAPI, for bare metal implementation and portability across platforms. Correctness in such an API is difficult to reason about manually, and testing against reference solutions is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control API internals to expose or reproduce errors. This paper provides a way to encode an MCAPI execution as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible execution schedule on the same trace, such that it resolves non-determinism in the MCAPI runtime in a way that it now fails user provided assertions. The paper proves the problem is NP-complete. The encoding is useful for test, debug, and verification of MCAPI program execution. The novelty in the encoding is the direct use of match pairs (potential send and receive couplings). Match-pair encoding for MCAPI executions, when compared to other encoding strategies, is simpler to reason about, results in significantly fewer terms in the SMT problem, and captures feasible behaviors that are ignored in previously published techniques. Further, to our knowledge, this is the first SMT encoding that is able to run in infinite-buffer semantics, meaning the runtime has unlimited internal buffering as opposed to no internal buffering. Results demonstrate that the SMT encoding, restricted to zero-buffer semantics, uses fewer clauses when compared to another zero-buffer technique, and it runs faster and uses less memory. As a result the encoding scales well for programs with high levels of non-determinism in how sends and receives may potentially match.

Currently, a single Unmanned Aerial System (UAS) requires several humans managing different aspects of the problem. Human roles often include vehicle operators, payload experts, and mission managers [1-3]. As a step toward reducing the number of humans required, it is desirable to reduce operator workload through effective distributed control, augmented autonomy, and intelligent user interfaces. Reliably doing this requires various roles in the system to be modeled. These roles naturally include the roles of the humans, but they also include roles delegated to autonomy and software decision-making algorithms, meaning the GUI and the unmanned aerial vehicle. This paper presents a conceptual model which models the roles of complex systems as a collection of actors, running in parallel. Results from applying this model to the UAS-enabled Wilderness Search and Rescue (WiSAR) domain indicate (a) it is possible to model the entire WiSAR system at varying degrees of abstraction (b) that building and evaluating the model provides insight into the best practices of WiSAR teams and (c) a way to model human machine interactions that works directly with the Java Pathfinder model checker to detect errors.

Coordination and synchronization of parallel tasks is a major source of complexity in parallel programming. These constructs take many forms in practice including directed barrier and point-to-point synchronizations, termination detection of child tasks, and mutual exclusion in accesses to shared resources.

This paper describes a tool to help debug error traces found by the Java Pathfinder model checker in concurrent Java programs. It does this by abstracting out thread interactions and program locations that are not obviously pertinent to the error through control flow or data dependence. The tool then iteratively refines the abstraction by adding thread interactions at critical locations until the error is reachable. The tool visualizes the entire process and enables the user to systematically analyze each abstraction and execution. Such an approach explicitly identifies specific context switch locations and thread interactions needed to debug a concurrent error trace in small to moderate programs that can be managed by the Java Pathfinder Tool.

Improper use of Inter-Process Communication (IPC) within concurrent systems often creates data races which can lead to bugs that are challenging to discover. Techniques that use Satisfiability Modulo Theories (SMT) problems to symbolically model possible executions of concurrent software have recently been proposed for use in the formal verification of software. In this work we describe a new technique for modeling executions of concurrent software that use a message passing API called MCAPI. Our technique uses an execution trace to create an SMT problem that symbolically models all possible concurrent executions and follows the same sequence of conditional branch outcomes as the provided execution trace. We check if there exists a satisfying assignment to the SMT problem with respect to specific safety properties. If such an assignment exists, it provides the conditions that lead to the violation of the property. We show how our method models behaviors of MCAPI applications that are ignored in previously published techniques.

A lack of scalable verification tools for concurrent programs has not allowed concurrent software development to keep abreast with hardware trends in multi-core technologies. The growing complexity of modern concurrent systems necessitates the use of abstractions in order to verify all the expected behaviors of the system. Current abstraction refinement techniques are restricted to verifying mostly sequential and simpler concurrent programs. In this work, we present a novel incremental underapproximation technique that uses program slicing. Based on a reachability property, an initial backward slice for a single thread is generated. The information in the program slice is coupled with a concrete execution to drive the lone thread; generating an underapproximation of the program behavior space. If the target location is reached in the underapproximation, then we have an actual concrete trace. Otherwise, the initial single-thread slice is refined to include another thread that affects the reachability of the target location. In this case, the concrete execution only considers the two threads in the slice and preemption points between the threads only occur at locations in the slice. This refinement process is repeated until the target location is reached or is shown to be unreachable. Initial results indicate that the incremental technique can potentially allow the discovery of errors in larger systems using fewer resources and produce a better reduction in systems that are correct.

We present a dynamic verification tool MCC for Multicore Communication API applications - a new API for communication among cores. MCC systematically explores all relevant interleavings of an MCAPI application using a tailor-made dynamic partial order reduction algorithm (DPOR). Our contributions are (i) a way to model the non-overtaking message matching relation underlying MCAPI calls with a high level algorithm to effect DPOR for MCAPI that controls the lower level details so that the intended executions happen at runtime; and (ii) a list of default safety properties that can be utilized in the process of verification. To our knowledge, this is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. Our result is the demonstration that we can indeed develop a dynamic model checker for MCAPI that can directly control the non-deterministic behavior at runtime that is inherent in any implementation of the library without additional API modifications or additions.

Exhaustive model checking search techniques are ineffective for error discovery in large and complex multi-threaded software systems. Distance estimate heuristics guide the concrete execution of the program toward a possible error location. The estimate is a lower-bound computed on a statically generated abstract model of the program that ignores all data values and only considers control flow. In this paper we describe a new distance estimate heuristic that efficiently computes a tighter lower-bound in programs with polymorphism when compared to the state of the art distance heuristic. We statically generate conservative distance estimates and refine the estimates when the targets of dynamic method invocations are resolved. In our empirical analysis the state of the art approach is computationally infeasible for large programs with polymorphism while our new distance heuristic can quickly detect the errors.

The relationship between changes in gene expression and physical characteristics associated with Down syndrome is not well understood. Chromosome 21 genes interact with nonchromosome 21 genes to produce Down syndrome characteristics. This indirect influence, however, is difficult to empirically define due to the number, size, and complexity of the involved gene regulatory networks. This work links chromosome 21 genes to non-chromosome 21 genes known to interact in a Down syndrome phenotype through a reachability analysis of labeled transition graphs extracted from published gene regulatory network databases. The analysis provides new relations in a recently discovered link between a specific gene and Down syndrome phenotype. This type of formal analysis helps scientists direct empirical studies to unravel chromosome 21 gene interactions with the hope for therapeutic intervention.

Directed model checking algorithms focus computation resources in the error-prone areas of concurrent systems. The algorithms depend on some empirical analysis to report their performance gains. Recent work characterizes the hardness of models used in the analysis as an estimated number of paths in the model that contain an error. This hardness metric is computed using a stateless random walk. We show that this is not a good hardness metric because models labeled hard with a stateless random walk metric have easily discoverable errors with a stateful randomized search. We present an analysis which shows that a hardness metric based on a stateful randomized search is a tighter bound for hardness in models used to benchmark explicit state directed model checking techniques. Furthermore, we convert easy models into hard models as measured by our new metric by pushing the errors deeper in the system and manipulating the number of threads that actually manifest an error.

State exploration in directed software model checking is guided using a heuristic function to move states near errors to the front of the search queue. Distance heuristic functions rank states based on the number of transitions needed to move the current program state into an error location. Lack of calling context information causes the heuristic function to underestimate the true distance to the error; however, inlining functions at call sites in the control flow graph to capture calling context leads to an exponential growth in the computation. This paper presents a new algorithm that implicitly inlines functions at call sites to compute distance data with unbounded calling context that is polynomial in the number of nodes in the control flow graph. The new algorithm propagates distance data through call sites during a depth-first traversal of the program. We show in a series of benchmark examples that the new heuristic function with unbounded distance data is more efficient than the same heuristic function that inlines functions at their call sites up to a certain depth

In this paper we build on the FSM distance heuristic for guided model checking by using the runtime stack to reconstruct calling context in procedural calls. We first build a more accurate static representation of the program by including a bounded level of calling context. We then use the calling context in the runtime stack with the more accurate control flow graph to estimate the distance to the possible error state. The heuristic is computed using both the dynamic and static construction of the program. We evaluate the new heuristic on models with concurrency errors. In these examples, experimental results show that for programs with function calls, the new heuristic better guides the search toward the error while the traditional FSM distance heuristic degenerates into a random search.

The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into modules, each with constrained complexity. Before verification is applied to each individual module, irrelevant information to the behavior of the selected module is abstracted away. This approach converts a verification problem with big exponential complexity to a set of subproblems, each with small exponential complexity. Experimental results are promising in that they indicate that our approach has the potential of completing much faster while using less memory than traditional flat analysis.

Using a level-oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model datapath circuits. On the other hand, in order to use such a model on large circuits, techniques to avoid the state explosion problem must be developed. This paper first introduces a level-oriented formal model based on time Petri nets, and then proposes its partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.

This paper presents a technique to estimate the stochastic cycle period (SCP), a performance metric for timed asynchronous circuits. This technique uses timed stochastic Petri nets (TSPN) which support choice and arbitrary delay distributions. The SCP is the delay of the average path in a TSPN when represented as a sum of weighted place delays. A place delay is the expected value of its associated distribution and its weight denotes its importance in the average path of the TSPN. The approach analyzes finite execution traces of the TSPN to derive an expression for the weight values in the SCP. The weights can be analyzed with basic statistics to within an arbitrary error bound. This paper demonstrates the use of the SCP to aggressively optimize timed asynchronous circuits for improved average-case performance by reducing transistor counts, reordering input pins at gates, and skewing transistor sizes to favor important transitions. Each optimization effort is directed to improve the average-case delay in the circuit at the possible expense of the worst-case delay.