NASA Formal Methods

For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error-free software. Available tools are often lacking in helping programmers develop more reliable and secure applications.

Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging.

This paper describes our experience in integrating a verification tool based on static analysis into the software development cycle at Facebook.

We present Leon, a system for developing functional Scala programs annotated with contracts. Contracts in Leon can themselves refer to recursively defined functions. Leon aims to find counterexamples when functions do not meet the specifications, and proofs when they do. Moreover, it can optimize run-time checks by eliminating statically checked parts of contracts and doing memoization. For verification Leon uses an incremental function unfolding algorithm (which could be viewed as k-induction) and SMT solvers. For counterexample finding it uses these techniques and additionally specification-based test generation. Leon can also execute specifications (e.g. functions given only by postconditions), by invoking a constraint solver at run time. To make this process more efficient and predictable, Leon supports deductive synthesis of functions from specifications, both interactively and in an automated mode. Synthesis in Leon is currently based on a custom deductive synthesis framework incorporating, for example, syntax-driven rules, rules supporting synthesis procedures, and a form of counterexample-guided synthesis. We have also developed resource bound invariant inference for Leon and used it to check abstract worst-case execution time. We have also explored within Leon a compilation technique that transforms real-valued program specifications into finite-precision code while enforcing the desired end-to-end error bounds. Recent work enables Leon to perform program repair when the program does not meet the specification, using error localization, synthesis guided by the original expression, and counterexample-guided synthesis of expressions similar to a given one. Leon is open source and can also be tried from its web environment at leon.epfl.ch.

This paper presents a formal description and analysis of a technique for distributed rollback recovery. The setting for this work is a model for data-parallel computation with a notion of virtual time. The technique allows the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks.

In the abstract interpretation theory, program properties are encoded by abstract domains, and the combination of abstract domains leads to new properties to be analyzed. We propose a new method to combine numerical abstract domains based on the Minkowski sum. We provide a general framework equipped with all the necessary abstract operators for static analysis of imperative languages.

The synthesis of timing parameters consists in deriving conditions on the timing constants of a concurrent system such that it meets its specification. Parametric timed automata are a powerful formalism for parameter synthesis, although most problems are undecidable. We first address here the following reachability preservation problem: given a reference parameter valuation and a (bad) control state, do there exist other parameter valuations that reach this control state iff the reference parameter valuation does? We show that this problem is undecidable, and introduce a procedure that outputs a possibly underapproximated answer. We then show that our procedure can efficiently replace the behavioral cartography to partition a bounded parameter subspace into good and bad subparts; furthermore, our procedure can even outperform the classical bad-state driven parameter synthesis semi-algorithm, especially when distributed on a cluster.

In this paper we address the problem of

uniform

verification of parameterised

timed

systems (PTS): “

does a given safety state property hold for a system containing n identical timed components regardless of the value of n?

”. Our approach is compositional and consequently it suits quite well such systems in that it presents the advantage of reusing existing local characterisations at the global level of system characterisation. Additionally, we show how a direct consequence of the modelling choices adopted in our framework leads to an elegant application of the presented method to topologies such as stars and rings.

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.

Symmetry reduction is one of the most successful techniques to cope with the state explosion problem in model-checking. One of the central issues in symmetry reduction is the problem of finding unique (canonical) representatives of equivalence classes of symmetric states. This problem is equivalent to the graph isomorphism problem, for which no polynomial algorithm is known. On the other hand finding multiple (non-canonical) representatives is much easier because it usually boils down to sorting algorithms. As a consequence, with multiple representatives one can significantly improve the verification times. In this paper we show that symmetry reduction with multiple representatives can be combined with partial order reduction, another efficient state space reduction technique. To this end we introduce a new weaker notion of independence which requires confluence only up to bisimulation.

We extend recent work by Höfner and McIver con the performances of the

ad hoc routing protocols

AODV and DYMO in terms of routes established. Höfner and McIver apply

statistical model checking

to show that on arbitrary small networks (up to 5 nodes) the most recent, and apparently more robust, DYMO protocol is less efficient than AODV. Here, we reformulate their experiments on 4x3 toroidal networks, with possibly lossy communication. As a main result we demonstrate that, in this more realistic scenario, DYMO performs significantly better than AODV.

Techniques for testing cyberphysical systems (CPS) currently use a combination of automatic directed test generation and random testing to find undesirable behaviors. Existing techniques can fail to efficiently identify bugs because they do not adequately explore the space of system behaviors. In this paper, we present an approach that uses the rapidly exploring random trees (RRT) technique to explore the state-space of a CPS. Given a Signal Temporal Logic (STL) requirement, the RRT algorithm uses two quantities to guide the search: The first is a robustness metric that quantifies the degree of satisfaction of the STL requirement by simulation traces. The second is a metric for measuring coverage for a dense state-space, known as the star discrepancy measure. We show that our approach scales to industrial-scale CPSs by demonstrating its efficacy on an automotive powertrain control system.

This paper presents an approach for proving the validity of first-order relational formulas that involve transitive closure. Given a formula

$$F$$

that includes the transitive closure of a relation

$$R$$

, our approach can deduce a complete (pure) first-order axiomatization of the paths of

$$R$$

that occur in

$$F$$

. Such axiomatization enables full automated verification of

$$F$$

using an automatic theorem prover like Z3. This is done via an iterative detection and injection of

$$R$$

-invariants —invariant formulas with respect to

$$R$$

-transitions in the context of

$$F$$

. This paper presents a proof for the correctness of the approach, and reports on its application to non-trivial Alloy benchmarks.

General hybrid systems can be difficult to verify due to their generality. To reduce the complexity, one often specializes to hybrid systems where the complexity is more manageable. If one reduces the modeling formalism to ones where the continuous variables have a single rate, then it may be possible to use the methods of

zones

to find the reachable state space. Zones are a restricted class of polyhedra formed by considering the intersections of half-planes defined by two variable constraints. Due to their simplicity, zones have simpler, more efficient methods of manipulation than more general polyhedral classes, though they are less accurate. This paper extends the method of zones to

labeled Petri net

(LPN) models with continuous variables that evolve over a range of rates.

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.

FDR is an explicit-state refinement checker for the process algebra CSP and, as such, is vulnerable to the state-explosion problem. In this paper, we show how a form of partial-order reduction, an automatic state reduction mechanism, can be utilised to soundly reduce the number of states that must be visited. In particular, we develop a compositional method for partial-order reduction that takes advantage of FDR’s internal, compositional, process representation. Further, we develop novel methods of preserving the traces of a process which allow partial-order reduction to be applied to arbitrary FDR refinement checks. We also provide details on how to efficiently implement the algorithms required for partial-order reduction.

The difficulty of writing test harnesses is a major obstacle to the adoption of automated testing and model checking. Languages designed for harness definition are usually tied to a particular tool and unfamiliar to programmers; moreover, such languages can limit expressiveness. Writing a harness directly in the language of the software under test (SUT) makes it hard to change testing algorithms, offers no support for the common testing idioms, and tends to produce repetitive, hard-to-read code. This makes harness generation a natural fit for the use of an unusual kind of domain-specific language (DSL). This paper defines a

template scripting

testing language, TSTL, and shows how it can be used to produce succinct, readable definitions of state spaces. The concepts underlying TSTL are demonstrated in Python but are not tied to it.

A prevalent asynchronous message passing standard is the Message Passing Interface (MPI). There are two runtime semantics for MPI: zero buffer (messages have no buffering) and infinite buffer (messages are copied into a runtime buffer on the API call). A problem in any MPI program, intended or otherwise, is zero buffer incompatibility. A zero buffer incompatible MPI program deadlocks. This problem is difficult to predict because a developer does not know if the deadlock is based on the buffering semantics or a bad program. This paper presents an algorithm that encodes a single-path MPI program as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible schedule, such that it proves the program is zero buffer compatible. This encoding is also adaptable to checking assertion violation for correct computation. To support MPI semantics, this algorithm correctly defines the point-to-point communication and collective communication with respective rules for both infinite buffer semantics and zero buffer semantics. The novelty in this paper is considering only the schedules that strictly alternate sends and receives leading to an intuitive zero buffer encoding. This paper proves that the set of all the strictly alternating schedules is capable of covering all the message communication that may occur in any execution under zero buffer semantics. Experiments demonstrate that the SMT encoding is correct and highly efficient for a set of benchmarks compared with two state-of-art MPI verifiers.

Dynamic languages are praised for their flexibility and expressiveness, but static analysis often yields many false positives and verification is cumbersome for lack of structure. Hence, unit testing is the prevalent incomplete method for validating programs in such languages.

Falsification is an alternative approach that uncovers definite errors in programs. A falsifier computes a set of inputs that definitely crash a program.

Success typing is a type-based approach to document programs in dynamic languages. We demonstrate that success typing is, in fact, an instance of falsification by mapping success (input) types into suitable logic formulae. Output types are represented by recursive types. We prove the correctness of our mapping (which establishes that success typing is falsification) and we report some experiences with a prototype implementation.

The paper considers the problem of model-based deployment of platform-independent control code on a specific platform. The approach is based on automatic generation of platform-specific glue code from an architectural model of the system. We present a tool, ROSGen, that generates the glue code based on a declarative specification of platform interfaces. Our implementation targets the popular Robot Operating System (ROS) platform. We demonstrate that the code generation process is amenable to formal verification. The code generator is implemented in Coq and relies on the infrastructure provided by the CompCert and VST tool. We prove that the generated code always correctly connects the controller function to sensors and actuators in the robot. We use ROSGen to implement a cruise control system on the LandShark robot.

We describe an approach to embedding a formal method within UML use case modelling. Moreover, we extend use case modelling to allow for the explicit representation of safety concerns. Our motivation comes from interaction with systems and safety engineers who routinely rely upon use case modelling during the early stages of defining and analysing system behaviours. Our chosen formal method is Event-B, which is refinement based and consequently has enabled us to exploit natural abstractions found within use case modelling. By underpinning informal use case modelling with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by safety engineers as well as the subsequent changes made at the level of use case modelling. To achieve this we have extended use case modelling to include the notion of an

accident case

. Our approach is currently being implemented, and we have an initial prototype.

Structural coverage metrics have traditionally categorized code as either covered or uncovered. Recent work presents a stronger notion of coverage,

checked coverage

, which counts only statements whose execution contributes to an outcome checked by an oracle. While this notion of coverage addresses the adequacy of the oracle, for Model-Based Development of safety critical systems, it is still not enough; we are also interested in how much of the oracle is covered, and whether the values of program variables are masked when the oracle is evaluated. Such information can help system engineers identify missing requirements as well as missing test cases. In this work, we combine results from checked coverage with results from requirements coverage to help provide insight to engineers as to whether the requirements or the test suite need to be improved. We implement a dynamic backward slicing technique and evaluate it on several systems developed in Simulink. The results of our preliminary study show that even for systems with comprehensive test suites and good sets of requirements, our approach can identify cases where more tests or more requirements are needed to improve coverage numbers.

For discrete-time probabilistic models there are efficient methods to check whether they satisfy certain properties. If a property is refuted, available techniques can be used to explain the failure in form of a counterexample. However, there are no

scalable

approaches to

repair

a model, i.e., to modify it with respect to certain side conditions such that the property is satisfied. In this paper we propose such a method, which avoids expensive computations and is therefore applicable to large models. A prototype implementation is used to demonstrate the applicability and scalability of our technique.

We present our integration of the Z3 SMT solver into the ACL2 theorem prover and its application to formal verification of analog-mixed signal circuits by proving global convergence for a state-of-the-art digital phase-locked loop (PLL). SMT (satisfiability modulo theory) solvers eliminate much of the tedium associated with detailed proofs by providing automatic reasoning about propositional formulas including equalities and inequalities of polynomial functions. A theorem prover complements the SMT solver by providing a proof structuring and proof by induction. We use this combined tool to show global convergence (i.e. correct start-up and mode-switching) of a digital PLL. The PLL is an example of a second-order hybrid control system; its verification demonstrates how these methods can address challenges that arise when verifying such designs.

Many formal method tools for increasing software reliability apply Satisfiability Modulo Theories (SMT) solvers to enumerate feasible paths in a program subject to certain coverage criteria. Examples include inconsistent code detection tools and concolic test case generators. These tools have in common that they typically treat the SMT solver as a black box, relying on its ability to efficiently search through large search spaces. However, in practice the performance of SMT solvers often degrades significantly if the search involves reasoning about complex control-flow. In this paper, we open the black box and devise a new algorithm for this problem domain that we call conflict-directed graph coverage. Our algorithm relies on two core components of an SMT solver, namely conflict-directed learning and deduction by propagation, and applies domain-specific modifications for reasoning about control-flow graphs. We implemented conflict-directed coverage and used it for detecting code inconsistencies in several large Java open-source projects with over one million lines of code in total. The new algorithm yields significant performance gains on average compared to previous algorithms and reduces the running times on hard search instances from hours to seconds.

We extend off-the-shelf shape analyses with the ability to infer numeric relations between directly or indirectly connected heap cells. Specifically, we introduce the concept of

connectors

, an instrumentation that retains relations between heap cells even if these cells are merged into summary nodes. Managing connectors is based on applying generic

$$\textit{fold}$$

and

$$\textit{expand}$$

operations on a numeric abstract domain. Connectors are thus a universal tool to enhance shape analyses with any numeric analysis. We show how connectors provide the ability to infer invariants of non-trivial heap structures such as sorted/skip lists and search trees.

Correct implementation of concurrent real-time systems has always been a tedious task due to their inherent complex structure; concurrency introduces a great deal of non-determinism, which can potentially conflict with meeting timing constraints. In this paper, we focus on model-based concurrent implementation of timed models. Our

abstract

models consist of a set of components interacting with each other using multi-party interactions. Each component is internally subject to a set of timing constraints. We propose a chain of transformations that starts with an abstract model as input and generates correct-by-construction executable code as output. We show that all transformed models are observationally equivalent to the abstract model through bisimulation proofs and, hence, all functional properties of the abstract model are preserved. To facilitate developing the proofs of correctness, each transformation obtains a model by incorporating a subset of

physical

constraints (e.g., type of communication and global clock synchronization)

PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to at least Common Criteria EAL5+, with “+” being applying formal methods compliant up to EAL7. We have formalized the hardware independent security-relevant part of PikeOS that is to be used in a certification context. Over this model, intransitive noninterference has been proven. We present the model and the methodology used to create the model. All results have been formalized in the Isabelle/HOL theorem prover.

In today’s internet-centric world, web applications have replaced desktop applications. Cloud systems are frequently used to store and manage user data. Given the complexity inherent in web applications, it is imperative to ensure that this data is never corrupted. We overview existing techniques for data model verification in web applications, list bugs discovered by these tools, and discuss the impact, difficulty of detection, and prevention of these bugs.

Detecting and debugging data races is a complex task due to the large number of interleavings possible in a parallel program. Most tools can find the data races reliably in an observed execution, but they miss errors in alternative reorderings of events. In this paper we describe an automated approach to generate, from a single program trace, a model in CSP with alternative interleavings. We check for data races patterns and obtain a witness that allows the reproduction of errors. Reproduction reduces the developer effort to correct the error.

Since about two decades, formal methods for continuous and hybrid systems enjoy increasing interest in the research community. A wide range of analysis techniques were developed and implemented in powerful tools. However, the lack of appropriate benchmarks make the testing, evaluation and comparison of those tools difficult. To support these processes and to ease exchange and repeatability, we present a manifold benchmark suite for the reachability analysis of hybrid systems. Detailed model descriptions, classification schemes, and experimental evaluations help to find the right models for a given purpose.

The HOL Multivariate Analysis Library (

HMA

) of Isabelle/HOL is focused on concrete types such as

$$\mathbb {R}$$

,

$$\mathbb {C}$$

and

$$\mathbb {R}^n$$

and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of

HMA

to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.

This paper describes a tool for intersecting context-free grammars. Since this problem is undecidable the tool follows a refinement-based approach and implements a novel refinement which is complete for regularly separable grammars. We show its effectiveness for safety verification of recursive multi-threaded programs.

We present the tool UFIT (

Uppaal Fault Injector for Timed automata

). In UFIT, we model five types of faults, namely, message loss, transient, byzantine, stuck-at, and fail-stop faults. Given the fault-free timed automata model and the selection of a type of fault, UFIT models the faults and generates the fault-affected timed automata model automatically. As a result, the designer can analyze the behavior of the model in the presence of faults. Moreover, there are several tools that extract timed automata models from higher-level programs. Hence, the designer can use UFIT to inject the faults into the extracted models.

We recently introduced a new proof system for Quantified Boolean Formulas (QBF), called QRAT, that opened up a variety of new preprocessing techniques. This paper presents a concept that follows from the QRAT proof system: blocked literals. Blocked literals are redundant universal literals that can be removed or added to clauses. We show that blocked literal elimination (

BLE

) and blocked literal addition are not confluent. We implemented

BLE

in the state-of-the-art preprocessor

bloqqer

. Our experimental results illustrate that the

BLE

extension improves solver performance on the 2014 QBF evaluation benchmarks.

An application developer’s primary task is to produce performant systems that meet their specifications. Formal methods techniques allow engineers to create models and implementations that have a high assurance of satisfying a specification. In this experience report, we take a model-based approach to software development that adds the assurance of formal methods to software construction while automating over 90% of the formal modeling. We discuss a software development methodology and two specific examples that illustrate how to integrate formal methods and their benefits into a traditional (testing-based) software development process.

Data races are a common type of bug found in multithreaded programs. The dynamic partial order reduction algorithm (DPOR) is an efficient algorithm for exploring a reduced set of interleavings that guarantees all assertion errors and deadlocks to be found. However, while DPOR does in effect explore different outcomes of data races, it was not originally designed to report them. In this paper a method for reporting data races during DPOR is presented. This allows data races to be found even when they do not trigger assertion errors or deadlocks. Additionally, for programs written in C++11 and a large subset of Java, the presented method allows DPOR to warn the user when it can not guarantee completeness due to the program having data races that trigger weak memory model semantics for it.