Finite-state verification techniques are often hampered by the state-explosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning, where a system under analysis is partitioned into subsystems and these subsystems are analyzed individually. By composing the results of these analyses, it can be determined whether or not the system satisfies a property. Because each subsystem is smaller than the whole system, analyzing each subsystem individually may reduce the overall cost of verification. Often the behavior of a subsystem is dependent on the subsystems with which it interacts, and thus it is usually necessary to provide assumptions about the environment in which a subsystem executes. Because developing assumptions has been a difficult manual task, the evaluation of assume-guarantee reasoning has been limited. Using recent advances for automatically generating assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks in these systems, we evaluated the decompositions as they were scaled. We found that in only a few cases can assume-guarantee reasoning verify properties on larger systems than monolithic verification can, and in these cases the systems that can be analyzed are only a few sizes larger. Although these results are discouraging, they provide insight about research directions that should be pursued and highlight the importance of experimental evaluation in this area.

Finite-state verification techniques are often hampered by the stateexplosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. Using recent advances in assume-guarantee reasoning that automatically generate assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks, we evaluated the decompositions as the systems were scaled. In only a few cases could assume-guarantee reasoning verify properties on larger systems than monolithic verification and, in these cases, assumeguarantee reasoning could only verify these properties on systems a few sizes larger than monolithic verification. This discouraging result, although preliminary, raises doubts about the usefulness of assume-guarantee reasoning.

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. To address the "state explosion" problem associated with this technique, we propose to integrate assume-guarantee verification at different phases of system development. During design, developers build abstract behavioral models of the system components and use them to establish key properties of the system. To increase the scalability of model checking at this level, we have previously developed techniques that automatically decompose the verification task by generating component assumptions for the properties to hold. The design artifacts are subsequently used to guide the implementation of the system, but also to enable more efficient reasoning of the source code. In particular, we propose to use assumptions generated for the design to similarly decompose the verification of the actual system implementation. We demonstrate our approach on a significant NASA application, where design models were used to identify and correct a safety property violation, and the generated assumptions allowed us to check successfully that the property was preserved by the implementation.

This article describes FLAVERS, a finite-state verification approach that analyzes whether concurrent systems satisfy user-defined, behavioral properties. FLAVERS automatically creates a compact, event-based model of the system that supports efficient dataflow analysis. FLAVERS achieves this efficiency at the cost of precision. Analysts, however, can improve the precision of analysis results by selectively and judiciously incorporating additional semantic information into an analysis.We report on an empirical study of the performance of the FLAVERS/Ada toolset applied to a collection of multitasking Ada systems. This study indicates that sufficient precision for proving system properties can usually be achieved and that the cost for such analysis typically grows as a low-order polynomial in the size of the system.

Software is increasingly expected to run in a variety of environments. The environments themselves are often dynamically changing when using mobile computers or embedded systems, for example. Network bandwidth, available power, or other physical conditions may change, necessitating the use of alternative algorithms within the software, and changing resource mixes to support the software. We present Containment Units as a software architecture useful for recognizing environmental changes and dynamically reconfiguring software and resource allocations to adapt to those changes. We present examples of Containment Units used within robotics along with the results of actual executions, and the application of static analysis to obtain assurances that those Containment Units can be expected to demonstrate the robustness for which they were designed.

Finite-state verification is emerging as an important technology for proving properties about software. In our experience, we have found that analysts have different expectations at different times. When an analyst is in an exploratory mode, initially formulating and verifying properties, analyses usually find inconsistencies because of flaws in the properties or in the software artifacts being analyzed. Once an inconsistency is found, the analyst begins to operate in a fault-finding mode, during which meaningful counter-example traces are needed to help determine the cause of the inconsistency. Eventually, systems become relatively stable, but still require re-verification as evolution occurs. During such periods, the analyst is operating in a maintenance mode and would expect re-verification to usually report consistent results. Although it could be that one algorithm suits all three of these modes of use, the hypothesis explored in this paper is that each would be best served by an algorithm optimized for the expectations of the analyst.

It seems imperative that the complex processes that syner-gize humans and computers to solve widening classes of societal problems be subjected to rigorous analysis. One approach is to use a process definition language to spec-ify these processes and to then use analysis techniques to evaluate these definitions for important correctness proper-ties. Because humans demand flexibility in their participa-tion in complex processes, process definition languages must incorporate complicated control structures, such as various concurrency, choice, reactive control, and exception mecha-nisms. Well-designed process languages provide powerful abstractions for concise and precise specification of such control, but balance this with visualization support to help users also obtain intuitive insights. The underlying complex-ity of these control abstractions, however, often confounds these intuitions as well as complicates any analysis. Thus, the control abstraction complexity in process def-inition languages presents analysis challenges beyond those posed by traditional programming languages. This paper ex-plores some of the difficulties of analyzing process defini-tions. Specifically, we explore issues arising when applying the FLAVERS finite state verification system to processes written in the Little-JIL process definition language and il-lustrate these issues using a realistic ecommerce auction ex-ample. Although we employ a particular process definition language and analysis technique, our results seem more gen-erally applicable.

Partial order optimization techniques for distributed systems improve the performance of finite state verification approaches by avoiding redundant exploration of some portions of the state space. Previously, such techniques have been applied in the context of model checking approaches. In this paper we propose a partial order optimization of the program model used by FLAVERS, a data flow based finite state verification approach for checking user-specified properties of distributed software. We demonstrate experimentally that this optimization often leads to significant reductions in the run time of the analysis algorithm of FLAVERS. On average, for those cases where this optimization could be applied, we observed a speedup of 21%. For one of the cases, the optimization resulted in an analysis speedup of 91%.