Search

Java Ranger is a path-merging tool for Java Programs. It identifies branching regions of code and summarizes them by generating a disjunctive logical constraint that describes the behavior of the code region. Previously, Java Ranger showed that a reduction of 70% of execution paths is possible when used to merge branching regions of code that support numeric constraints.In this paper, we describe the support of two additional features since participation in SV-COMP 2020: symbolic array and symbolic string operations. Finally, we present a preliminary evaluation of the effect of the structure of the disjunctive constraint on the solver’s performance. Results suggest that certain constraint structures can speed up the performance of Java Ranger.

Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which has limited their use in critical applications. In this paper, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. Our approach is more scalable and general than previous explorations for parallel clause-sharing solvers, allowing use on distributed solvers without shared memory. We propose a simple sequential algorithm as well as a fully distributed algorithm for proof composition. Our empirical evaluation shows that for large-scale distributed solvers (100 nodes of 16 cores each), our distributed approach allows reliable proof composition and checking with reasonable overhead. We analyze the overhead and discuss how and where future efforts may further improve performance.

Symbolic model checkers can construct proofs of properties over highly complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, measure completeness of a set of requirements over a model, and assist with design optimization given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute inductive validity cores (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current SMT solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as all inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.

Formal methods are mathematically based approaches for specifying, building, and reasoning about software. Despite 50 years of research and development, formal methods have had only limited impact in industry. While we have seen success in such domains as microprocessor design and aerospace (e.g., proofs of security properties for helicopter control systems1), we have not seen wide adoption of formal methods for large and complex systems, such as web services, industrial automation, or enterprise support software.

Safety analysis is used to ensure that critical systems operate within some level of safety when failures are present. As critical systems become more dependent on software components, it becomes more challenging for safety analysts to comprehensively enumerate all possible failure causation paths. Any automated analyses should be sound to sufficiently prove that the system operates within the designated level of safety. This paper presents a compositional approach to the generation of fault forests (sets of fault trees) and minimal cut sets. We use a behavioral fault model to explore how errors may lead to a failure condition. The analysis is performed per layer of the architecture and the results are automatically composed. A complete formalization is given. We implement this by leveraging minimal inductive validity cores produced by an infinite state model checker. This research provides a sound alternative to a monolithic framework. This enables safety analysts to get a comprehensive enumeration of all applicable fault combinations using a compositional approach while generating artifacts required for certification.

Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java. Because Java code typically contains many small dynamically dispatched methods, it is important to include them in multi-path regions; we introduce dynamic inlining of method-regions to do so modularly. Java’s typed memory structure is very different from the binary representation, but we show how the idea of static single assignment (SSA) form can be applied to object references to statically account for aliasing. We have implemented our algorithms in Java Ranger, an extension to the widely used Symbolic Pathfinder tool. In a set of nine benchmarks, Java Ranger reduces the running time and number of execution paths by a total of 38% and 71% respectively as compared to SPF. Our results are a significant improvement over the performance of JBMC, a recently released verification tool for Java bytecode. We also participated in a static verification competition at a top theory conference where other participants included state-of-the-art Java verifiers. JR won first place in the competition’s Java verification track.

Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

Current approaches to cyberresiliency rely on patching systems after a vulnerability is discovered. What is needed is a clean-slate, mathematically based approach for building secure software. We developed new tools based on formal methods for building software for unmanned air vehicles that is provably secure against cyberattacks.

Scaling symbolic execution to industrial-sized programs is an important open research problem. Veritesting is a promising technique that improves scalability by combining the advantages of static symbolic execution with those of dynamic symbolic execution. The goal of veritesting is to reduce the number of paths to explore in symbolic execution by creating formulas describing regions of code using disjunctive formulas. In previous work, veritesting was applied to binary-level symbolic execution. Integrating veritesting with Java bytecode presents unique challenges: notably, incorporating non-local control jumps caused by runtime polymorphism, exceptions, native calls, and dynamic class loading. If these language features are not accounted for, we hypothesize that the static code regions described by veritesting are often small and may not lead to substantial reduction in paths. We examine this hypothesis by running a Soot-based static analysis on six large open-source projects used in the Defects4J collection. We find that while veritesting can be applied in thousands of regions, allowing static symbolic execution involving non-local control jumps amplifies the performance improvement obtained from veritesting. We hope to use these insights to support efficient veritesting in Symbolic PathFinder in the near future. Toward this end, we brie y address some engineering challenges to add veritesting into SPF.

Model-based engineering tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs, and providing accurate results throughout the system life-cycle. In this paper we describe an extension to the Architecture Analysis and Design Language (AADL) that supports modeling of system behavior under failure conditions. This safety annex enables the independent modeling of component failures and allows safety engineers to weave various types of fault behavior into the nominal system model. The accompanying tool support uses model checking to verify safety properties in the presence of faults and comprehensively enumerate all applicable fault combinations leading to failure conditions under quantitative objectives as part of the safety assessment process. The approach allows exploration of the effects of faulty component behavior on system level failure conditions without requiring explicit propagation specifications. It also supports a shared system model, a modeling language that can describe real-time embedded systems, and usable safety analysis artifacts.

In the High-Assurance Cyber Military Systems project, researchers are investigating how to construct complex networked-vehicle software securely. Experiments demonstrated that careful attention to requirements and system architecture, along with formally verified approaches that remove known security weaknesses, can lead to vehicles that can withstand attacks from even sophisticated attackers with access to vehicle design data. The Web extra at https://youtu.be/EvG7fjdvyro is an audio podcast of author Michael W. Whalen reading the column that he cowrote with Darren Cofer and Andrew Gacek.

JKind is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKind uses multiple parallel engines to prove or falsify safety properties of infinite state models. It is portable, easy to install, performance competitive with other state-of-the-art model checkers, and has features designed to improve the results presented to users: inductive validity cores for proofs and counterexample smoothing for test-case generation. It serves as the back-end for various industrial applications.

Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of \(\forall \exists \)-formulas. In spirit of IC3/PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKind’s already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Minimal Inductive Validity Cores (MIVCs) trace a property to a minimal set of model elements necessary for constructing a proof, and can help to explain why a property is true of a model. In addition, the traceability information provided by MIVCs can be used to perform a variety of engineering analysis such as coverage analysis, robustness analysis, and vacuity detection. The more MIVCs are identified, the more precisely such analyses can be performed. Nevertheless, a full enumeration of all MIVCs is in general intractable due to the large number of possible model element sets. The bottleneck of existing algorithms is that they are not guaranteed to emit minimal IVCs until the end of the computation, so returned results are not known to be minimal until all solutions are produced.

Editor’s notes: Safety critical systems such as cruise control in automotive systems and variable rate bolus in medical device infusion pumps introduce complexity and reduce the flexibility of incremental code modifications. This paper proposes a generic pattern to structure the mode logic such that additions, modifications, and removal of behaviors could be done in a quick and localized fashion without losing model integrity. The authors illustrate the proposed pattern using the infusion pump as a case study and describe a design pattern for the mode logic of reactive systems that allows for flexible, understandable, and maintainable models.

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Recently, proof cores (alternately, for inductive model checkers, Inductive Validity Cores (IVCs)) were introduced to trace a property to a minimal set of model elements necessary for proof. Minimal IVCs facilitate several engineering tasks, including performing traceability and analyzing requirements completeness, that usually rely on the minimality of IVCs. However, existing algorithms for generating an IVC are either expensive or only able to find an approximately minimal IVC. Besides minimality, computing all minimal IVCs of a given property is an interesting problem that provides several useful analyses, including regression analysis for testing/proof, determination of the minimum (as opposed to minimal) number of model elements necessary for proof, the diversity examination of model elements leading to proof, and analyzing fault tolerance. This paper proposes an efficient method for finding all minimal IVCs of a given property proving its correctness and completeness. We benchmark our algorithm against existing IVC-generating algorithms and show, in many cases, the cost of finding all minimal IVCs by our technique is similar to finding a single minimal IVC using existing algorithms.

When using formal verification on critical software, an important question involves whether the properties used for analysis are sufficient to adequately constrain the behavior of an implementation model. To address this question, coverage metrics for property-based formal verification have been proposed. Existing metrics are usually based on mutation, where the implementation model is repeatedly modified and re-analyzed to determine whether mutant models are ``killed'' by the property set. These metrics tend to be very expensive to compute, as they involve many additional verification problems. This paper proposes an alternate family of metrics that can be computed using the recently introduced idea of Inductive Validity Cores (IVCs). IVCs determine a minimal set of model elements necessary to establish a proof. One of the proposed metrics is both rigorous and substantially cheaper to compute than mutation-based metrics. In addition, unlike the mutation-based techniques, the design elements marked as necessary by the metric are guaranteed to preserve provability. We demonstrate the metrics on a large corpus of examples.

Architecture description languages such as AADL allow systems engineers to specify the structure of system architectures and perform several analyses over them, including schedulability, resource analysis, and information flow. In addition, they permit system-level requirements to be specified and analyzed early in the development process of airborne and ground-based systems. These tools can also be used to perform safety analysis based on the system architecture and initial functional decomposition.

The advanced use of technology in medical devices has improved the way health care is delivered to patients. Unfortunately, the increased complexity of modern medical devices poses challenges for development, assurance, and regulatory approval. In an effort to improve the safety of advanced medical devices, organizations such as FDA have supported exploration of techniques to aid in the development and regulatory approval of such systems. In an ongoing research project, our aim is to provide effective development techniques and exemplars of system development artifacts that demonstrate state of the art development techniques.

Systems are naturally constructed in hierarchies, in which design choices made at higher levels of abstraction levy requirements on system components at the lower levels. Thus, whether an aspect of a system is a design choice or a requirement largely depends on your vantage point within the system components' hierarchy. Systems are also often constructed from the middle-out rather than top-down; compatibility with existing systems and architectures and availability of specific components influence high-level requirements. Requirements and architectural design should be more closely aligned: requirements models must account for hierarchical system construction and architectural design notations must better support requirements specification for system components.

Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, and can also be used to measure completeness of a set of requirements over a model. In this paper, we present a new algorithm to efficiently compute the inductive validity core (IVC) within a model necessary for inductive proofs of safety properties for sequential systems. The algorithm is based on the UNSAT core support built into current SMT solvers and a novel encoding of the inductive problem to try to generate a minimal inductive validity core. We prove our algorithm is correct, and describe its implementation in the JKind model checker for Lustre models. We then present an experiment in which we benchmark the algorithm in terms of speed, diversity of produced cores, and minimality, with promising results., appears in FSE2016: ACM Sigsoft International Symposium on the Foundations of Software Engineering, Seattle, WA, November 13-19, 2016

When establishing associations, known as tracelinks, between a requirement and the artifacts that lead to itssatisfaction, it is essential to know what the links mean. Whileresearch into this type of traceability—what we call RequirementsSatisfaction Traceability—has been an active research area forsome time, none of the literature discusses the fact that thereare often multiple ways in which a requirement can be satisfied, i.e., there are multiple satisfaction arguments. The distinctionbetween establishing a single satisfaction argument between arequirement and its implementation (tracing one way the requirement is implemented) vs. tracing all satisfaction arguments, and the possible ramifications for how the trace links can beused in analysis, has not been well studied. We examine how thisdistinction changes the way traceability is perceived, established, maintained, and used. In this RE@Next! paper, we introduce anddiscuss the notion of "complete" traceability, which considersall trace links between the requirements and the artifacts thatwork to satisfy the requirements, and contrast it with the partialtraceability common in practice.

In previous work, we have introduced a contract-based real- izability checking algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arith- metic and uninterpreted functions over infinite domains. This algorithm can determine whether or not it is possible to con- struct a realization (i.e. an implementation) of an assume- guarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to deter- mine implementability. While our work on realizability is inherently useful for vir- tual integration in determining whether it is possible for sup- pliers to build software that meets a contract, it also provides the foundations to solving the more challenging problem of component synthesis. In this paper, we provide an initial synthesis algorithm for assume-guarantee contracts involv- ing infinite theories. To do so, we take advantage of our realizability checking procedure and a skolemization solver for forall-exists formulas, called AE-VAL. We show that it is possible to immediately adapt our existing algorithm towards syn- thesis by using this solver, using a demonstration example. We then discuss challenges towards creating a more robust synthesis algorithm., Comment: 6 pages, 1 figure

Intelligent controller designs based on artificial intelligence and machine learning promise superior performance over traditional control techniques; however, the lack of transparency in intelligent control systems and the opportunity for emergent behaviors limits where these systems may be applied. Run Time Assurance (RTA) is a proposed methodology to allow intelligent (unverified) controllers to perform within a predetermined envelope of acceptable behavior. Rather than depending entirely on offline verification, RTA provides an online verification approach. Based on the Simplex Architecture, RTA architectures use a decision module to monitor control system performance and switch control from an unverified controller to a verified backup controller if the unverified controller violates acceptable behavior ranges or is forced to operate outside of predetermined conditions. The focus of this work is to combine formal methods analysis with an RTA architecture to generate proof that the output of the RTA controller does not violate safety properties. A 6U CubeSat attitude control subsystem case study is presented and formal methods are used to prove the outputs of the verified controller, decision module, and the larger RTA control system never violate a set of safety properties describing actuator limitations.

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions, assume/guarantee contracts, and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction. For these proofs to be meaningful, each leaf-level component contract must be realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. We have recently proposed ini¾ź[1] a contract-based realizability checking algorithm for assume/guarantee contracts over infinite theories supported by SMT solvers such as linear integer/real arithmetic and uninterpreted functions. In that work, we used an SMT solver and an algorithm similar to k-induction to establish the realizability of a contract, and justified our approach via a hand proof. Given the central importance of realizability to our virtual integration approach, we wanted additional confidence that our approach was sound. This paper describes a complete formalization of the approach in the Coq proof and specification language. During formalization, we found several small mistakes and missing assumptions in our reasoning. Although these did not compromise the correctness of the algorithm used in the checking tools, they point to the value of machine-checked formalization. In addition, we believe this is the first machine-checked formalization for a realizability algorithm.

English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification language is often challenging, especially if the specification language does not contain constructs analogous to those used in the original requirements. For example, requirements often contain real-time constraints, but many specification languages for model checkers have discrete time semantics. Work in specification patterns helps to bridge these gaps, allowing straightforward expression of common requirements patterns in formal languages. In this work we demonstrate how we support real-time specification patterns in the Assume Guarantee Reasoning Environment AGREE using observers. We demonstrate that there are subtle challenges, not mentioned in previous literature, to express real-time patterns accurately using observers. We then demonstrate that these patterns are sufficient to model real-time requirements for a real-world avionics system.

Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain. We show that the procedure is sound and complete for a class of catamorphisms that satisfy a generalized sufficient surjectivity condition. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We use the generalized sufficient surjectivity condition to address an incompleteness in the previous unrolling algorithm (and associated proof). We then propose the categories of monotonic and associative catamorphisms, which we argue provide a more intuitive inclusion test than the generalized sufficient surjectivity condition. We use these notions to address two open problems from previous work: (1) we provide a bound, with respect to formula size, on the number of unrollings necessary for completeness, showing that it is linear for monotonic catamorphisms and exponentially small for associative catamorphisms, and (2) we demonstrate that associative catamorphisms can be combined within a formula while preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-LIB 2.0 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards., Comment: To appear in Journal of Automated Reasoning

Guardol is a domain-specific language focused on the creation of high-assurance network guards and the specification of guard properties. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.

A translator framework enables the use of model checking in complex avionics systems and other industrial settings.

This paper describes an extension to Lustre to support the analysis of globally asynchronous, locally synchronous (GALS) architectures. This extension consists of constructs for directly specifying the timeout automata used to describe asynchronous communication between processes represented by Lustre nodes. It is implemented using an extensible language framework based on attribute grammars that allows such extensions to be modularly defined so that they may be more easily composed with other language extensions.

To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. High-level analysis explores interactions of the system with its physical environment, while embedded software is developed separately based on derived requirements. This separation of low-level and high-level analysis also gives hope to scalability, because we are able to use tools that are appropriate for each level. When attempting to perform compositional reasoning in such an environment, care must be taken to ensure that results from one tool can be used in another to avoid errors due to “mismatches” in the semantics of the underlying formalisms. This paper proposes a formal approach for linking high-level continuous time models and lower-level discrete time models.

Exhaustive test of complex and autonomous systems is intractable and cost prohibitive; however, incorporating formal methods analysis throughout the system design process provides a means to identify faults as they are introduced and drastically reduce the overall system development cost. Software errors on fielded spacecraft have resulted in catastrophic faults that could have been prevented had formal methods been applied to the system design. In this research, formal methods, such as model checking and limited theorem proving, are applied to the requirements, architecture, and model development phases of the design process of a reaction wheel attitude control system for a 6U CubeSat. The results show that while feasible, several gaps exist in the capability of formal methods analysis tools. The tools are capable of expressing and analyzing some of the properties of the system, but more work is needed to properly address inherent nonlinearities in complex systems.

In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA’s Transport Class Model (TCM). We use a compositional approach with assume-guarantee contracts that correspond to the requirements for software components embedded in an AADL system architecture model. This approach is designed to exploit the verification effort and artifacts that are already part of typical software verification processes in the avionics domain. Our approach is supported by an AADL annex that allows specification of contracts along with a tool, called AGREE, for performing compositional verification. The goal of this paper is to show the benefits of a compositional verification approach applied to a realistic avionics system and to demonstrate the effectiveness of the AGREE tool in performing this analysis.

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction. Such proofs build from “leaf-level” assume/guarantee component contracts through architectural layers towards top-level safety properties. The proofs are built upon the premise that each leaf-level component contract is realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. Without engineering support it is all too easy to write leaf-level components that can’t be realized. Realizability checking for propositional contracts has been well-studied for many years, both for component synthesis and checking correctness of temporal logic requirements. However, checking realizability for contracts involving infinite theories is still an open problem. In this paper, we describe a new approach for checking realizability of contracts involving theories and demonstrate its usefulness on several examples.

Incomplete, inaccurate, ambiguous, and vola-tile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach to the early validation of requirements. This paper describes an exercise conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical flight guidance system were captured as natural language “shall” statements. A formal model of the mode logic was written in the RSML−e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each “shall” statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML−e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation.

Inaccuracies, or deviations, in the measurements of monitored variables in a control system are facts of life that control software must accommodate. Deviation analysis can be used to determine how a software specification will behave in the face of such deviations. Deviation analysis is intended to answer questions such as "What is the effect on output O if input I is off by 0 to 100?". This property is best checked with some form of symbolic execution approach. In this report we wish to propose a new approach to deviation analysis using model checking techniques. The key observation that allows us to use model checkers is that the property can be restated as "Will there be an effect on output O if input I is off by 0 to 100?"--this restatement of the property changes the analysis from an exploratory analysis to a verification task suitable for model checking.

Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.

Model-based development (MBD) tool suites such as Simulink and Stateflow offer powerful tools for design, development, and analysis of models. These models can be used for several purposes: for code generation, for prototyping, as descriptions of an environment (plant) that will be controlled by software, as oracles for a testing process, and many other aspects of software development. In addition, a goal of model-based development is to develop reusable models that can be easily managed in a version-controlled continuous integration process. Although significant guidance exists for proper structuring of source code for these purposes, considerably less guidance exists for MBD approaches. In this paper, we discuss structuring issues in constructing models to support use (and reuse) of models for design and verification in critical software development projects. We illustrate our approach using a generic patient-controlled analgesia infusion pump (GPCA), a medical cyber-physical system.

Structural coverage criteria have been proposed to measure the adequacy of testing efforts. Indeed, in some domains—e.g., critical systems areas—structural coverage criteria must be satisfied to achieve certification. The advent of powerful search-based test generation tools has given us the ability to generate test inputs to satisfy these structural coverage criteria. While tempting, recent empirical evidence indicates these tools should be used with caution, as merely achieving high structural coverage is not necessarily indicative of high fault detection ability. In this report, we review some of these findings, and offer recommendations on how the strengths of search-based test generation methods can alleviate these issues.

System requirements and system architecture/design co-evolve as the understanding of both the problem at hand as well as the solution to be deployed evolve---the Twin Peaks concept. Modeling of requirements and solution is a promising approach for exploring the Twin Peaks. Commonly, such models are deterministic because of the choice of modeling notation and available analysis tools. Unfortunately, most systems operate in an uncertain environment and contain physical components whose behaviors are stochastic. Although much can be learned from modeling and analysis with commonly used tools, e.g., Simulink/Stateflow and the Simulink Design Verifier, the SCADE toolset, etc., the results from the exploration of the Twin Peaks will---by necessity---be inaccurate and can be misleading; inclusion of the probabilistic behavior of the physical world provides crucial additional insight into the system's required behavior, its operational environment, and the solution proposed for its software. Here, we share our initial experiences with model-based deterministic and probabilistic verification approaches while exploring the Twin Peaks. The intent of this paper is to demonstrate how probabilistic reasoning helps illuminate weaknesses in system requirements, environmental assumptions, and the intended software solution, that could not be identified when using deterministic techniques. We illustrate our experience through a medical device subsystem, modeled and analyzed using the Simulink/Stateflow (deterministic) and PRISM (probabilistic) tools.

To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. Formal reasoning about such systems, therefore, usually involves multiple modeling formalisms, verification paradigms, and associated tools. System properties verified using an abstract component specification in one paradigm must be shown to logically follow from properties verified --- possibly using a different paradigm --- on a more concrete component description. As component specifications at one layer of abstraction get elaborated into more concrete component descriptions at the next lower level, abstraction induced differences come to the fore; differences that have to be reconciled. In this paper, we present an approach to tie together distinct verification paradigms and reconcile these abstraction induced differences using a medical device cyber-physical system as an example. While the specifics are particular to the example at hand, we believe the techniques are applicable in similar situations for verifying cyber-physical system properties.

Reasoning about algebraic data types and functions that operate over these data types is an important problem for a large variety of applications. In this paper, we present a decision procedure for reasoning about data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends a previous decision procedure that solves formulas involving algebraic data types via successive unrollings of catamorphism functions. First, we propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to fix an incompleteness in the previous unrolling algorithm and associated proof. We then use these notions to address two open problems from previous work: 1 we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and 2 we demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness.

Systems are naturally constructed in hierarchies in which design choices made at higher levels of abstraction ``flow down'' to requirements on system components at lower levels of abstraction. Thus, whether an aspect of the system is a design choice or a requirement depends largely on one's vantage point within the hierarchy of system components. Furthermore, systems are often constructed middle-out rather than top-down; compatibility with existing systems and architectures, or availability of specific components influences high-level requirements. We believe that requirements and architectural design should be more closely aligned: that requirements models must account for hierarchical system construction, and that architectural design notations must better support specification of requirements for system components.In this presentation, I describe tools supporting iterative development of architecture and verification based on software models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification. To describe and verify component-level behavior, we use Simulink and Stateflow and multiple analysis tools.

Complex systems are by necessity hierarchically organized. Decomposition into subsystems allows for intellectual control, as well as enabling different subsystems to be created by distinct teams. This decomposition affects both requirements and architecture. The architecture describes the structure and this affects how requirements ``flow down'' to each subsystem. Moreover, discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. In this paper, we present a medical device case example where we apply an iterative approach to architecture and verification based on software architectural models. We represent the hierarchical composition of the system in the Architecture Analysis and Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design and verification of detailed behavioral models, and to scale formal analysis to large software systems.

Symbolic execution is a program analysis technique that attempts to explore all possible paths through a program by using symbolic values rather than actual data values as inputs. When applied to Statecharts, a model-based formalism for reactive systems, symbolic execution can determine all feasible paths through a model up to a specified bound and generate input sequences exercising these paths. The main drawback of this method is its computational expense. This paper describes two efforts to improve the performance of symbolic execution within our previously developed framework for Statechart analysis. One method is a multithreaded symbolic execution engine targeted directly at our framework. A second, orthogonal, method is program specialization with respect to a particular model and Statechart semantics, which uses symbolic execution to rewrite the original code into an equivalent form that has fewer instructions and is easier to analyze.

Systems are naturally constructed in hierarchies in which design choices made at higher levels of abstraction levy requirements on system components at lower levels of abstraction. Thus, whether an aspect of the system is a design choice or a requirement depends largely on one's location within the hierarchy of system components. In addition, it is often the case that systems are not constructed top-down, but rather middle-out; compatibility with existing systems and architectures, or availability of specific physical components may influence high-level requirements. Despite these facts, several of the reference models commonly used for requirements, including the four-variable model and world machine model, do not account for hierarchical decomposition. In this position paper, we argue that requirements and architectural design should be more closely aligned: that requirements reference models should account for hierarchical system construction, and that architectural design notations should better support specification of requirements for system components. We briefly describe work to this end that was performed on the META II project and describe the gaps in this work that need to be addressed to meet practitioner needs.