We reflect on the impact of software verification techniques, as implemented in the logic model checking tool SPIN, on the development of modern safety critical software systems and reflect on future developments in the application of formal verification techniques, especially in the context of the new generation of AI-based systems and tools.

Developing and maintaining a file system is time-consuming, typically requiring years of effort. Developers often test compliance with APIs such as POSIX with hand-written regression suites that, alas, examine only a fraction of a file system's state space. Conversely, formal model checking can explore vast state spaces efficiently, increasing confidence in the file system's implementation. Yet model checking is not currently part of file system development. Our position is that file systems should be designed a priori to facilitate model checking. To this end, we introduce MCFS, an architecture for efficient and comprehensive file-system model checking. MCFS relies on two new APIs that save and restore a file system's in-memory and on-disk state. We describe our earlier attempts at model-checking file systems, including unsuccessful or inefficient ones. Those attempts led us to develop VeriFS, which implements the new APIs. We illustrate MCFS's model-checking principles with VeriFS, a FUSE-based file system we were able to quickly develop with MCFS's help.

Current static source code analyzers can be slow, hard to use correctly, and expensive. If not properly configured, they can also generate large amounts of output, even for well-written code. To fix this, we developed a new tool called Cobra. The Cobra tool can be used interactively even on very large code bases, which means that it is very fast. It is also designed to be easy to use and free.

Sadly we know that virtually all software of any significance has residual errors. Some of those errors can be traced back to requirements flaws or faulty design assumptions; others are just plain coding mistakes. Static analyzers have become quite good at spotting these types of errors, but they don't scale very well. If, for instance, you need to check a code base of a few million lines you better be prepared to wait for the result; sometimes hours. Eyeballing a large code base to find flaws is clearly not an option, so what is missing is a static analysis capability that can be used to answer common types of queries interactively, even for large code bases. I will describe the design and use of such a tool in this talk.

In software analysis most research has traditionally been focused on the development of tools and techniques that can be used to formally prove key correctness properties of a software design. Design errors can be hard to catch without the right tools, and even after decades of development, the right tools can still be frustratingly hard to use.

This paper extends the piggyback algorithm to enlarge the set of liveness properties it can verify. Its extension is motivated by an attempt to express in logic the counterexamples it can detect and relate them to bounded liveness. The original algorithm is based on parallel breadth-first search and piggybacking of accepting states that are deleted after counting a fixed number of transitions. The main improvement is obtained by renewing the counter of transitions when the same accepting states are visited in the negated property automaton. In addition, we describe piggybacking of multiple states in either sets (exact) or Bloom filters (lossy but conservative), and use of local searches that attempt to connect cycles fragmented among processing cores. Finally it is proved that accepting cycle detection is in NC in the size of the product automaton's entire state space, including unreachable states.

Is quality really free? Often, but not in many situations. Are organizations getting the best value for their investments in reliability? Frequently not. If different stakeholders are relying on the system and software for different properties, is there a single reliability metric to manage to? Frequently not. Is reliability affected by decisions on other system and software ilities? Often quite seriously. This talk will review a number of data sources, case studies, calibrated models, and recent research on systems and software ility tradeoffs to suggest ways that can help improve an organization's return on investments in more reliable systems and software.

We describe a certification approach for software development that has been adopted at our organization. JPL develops robotic spacecraft for the exploration of the solar system. The flight software that controls these spacecraft is considered to be mission critical. We argue that the goal of a software certification process cannot be the development of "perfect" software, i.e., software that can be formally proven to be correct under all imaginable and unimaginable circumstances. More realistically, the goal is to guarantee a software development process that is conducted by knowledgeable engineers, who follow generally accepted procedures to control known risks, while meeting agreed upon standards of workmanship. We target three specific issues that must be addressed in such a certification procedure: the coding process, the code that is developed, and the skills of the coders. The coding process is driven by standards. The code is mechanically checked against the standards with the help of state-of-the-art static source code analyzers. The coders, finally, are certified in on-site training courses that include formal exams.

In the verification of multitask software in real-time embedded systems, general purpose model checkers do not inherently consider characteristics of the real-time operating system, such as priority-based scheduling, priority inversion, and protocols for protecting shared memory resources. Since explicit state model checkers generally explore all possible execution paths and task interleaving, this could potentially lead to exploring execution paths that are redundant, unnecessarily increasing verification complexity and hampering tractability. Based on this premise, in this work we investigate how one can improve the performance of explicit state model checkers, such as SPIN, for the verification of multitask applications that target real-time operating systems.

Abstract We discuss the implementation of a bounded context switching algorithm in the Spin model checker. The algorithm allows us to find counter-examples that are often simpler to understand, and that may be more likely to occur in practice. We discuss extensions of the algorithm that allow us to use this new algorithm in combination with most other search modes supported in Spin, including partial order reduction and bitstate hashing. We show that, other than often assumed, the enforcement of a bounded context switching discipline does not decrease but increases the complexity of the model checking procedure. We discuss the performance of the algorithm on a range of applications.

The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances and new theoretical insights, but it has also benefitted from the steady increase in processing speeds and main memory sizes on standard computers. The steady increase in processing speeds, though, ended when chip-makers started redirecting their efforts to the development of multicore systems. For the near-term future, we can anticipate the appearance of systems with large numbers of CPU cores, but without matching increases in clock-speeds. We will describe a model checking strategy that can allow us to leverage this trend and that allows us to tackle significantly larger problem sizes than before.

Reportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow afield than a thousand chickens. Although this is undoubtedly wise when it comes to plowing afield, it is not so clear for other types of tasks. Model checking problems are of the proverbial "search the needle in a haystack" type. Such problems can often be parallelized easily. Alas, none of the usual divide and conquer methods can be used to parallelize the working of a model checker. Given that it has become easier than ever to gain access to large numbers of computers to perform even routine tasks it is becoming more and more attractive to find alternate ways to use these resources to speed up model checking tasks. This paper describes one such method, called swarm verification.

Most flight software testing at the Jet Propulsion Laboratory relies on the use of hand-produced test scenarios and is executed on systems as similar as possible to actual mission hardware. We report on a flight software development effort incorporating large-scale (biased) randomized testing on commodity desktop hardware. The results show that use of a reference implementation, hardware simulation with fault injection, a testable design, and test minimization enabled a high degree of automation in fault detection and correction. Our experience will be of particular interest to developers working in domains where on-time delivery of software is critical (a strong argument for randomized automated testing) but not at the expense of correctness and reliability (a strong argument for model checking, theorem proving, and other heavyweight techniques). The effort spent in randomized testing can prepare the way for generating more complete confidence using heavyweight techniques.

We present the first experimental results on the implementation of a multi-core model checking algorithm for the SPIN model checker. These algorithms specifically target shared-memory systems, and are initially restricted to dual-core systems. The extensions we have made require only small changes in the SPIN source code, and preserve virtually all existing verification modes and optimization techniques supported by SPIN, including the verification of both safety and liveness properties and the verification of SPIN models with embedded C code fragments.

Abstract We propose tackling a “mini challenge” problem: a nontrivial verification effort that can be completed in 2–3 years, and will help establish notational standards, common formats, and libraries of benchmarks that will be essential in order for the verification community to collaborate on meeting Hoare’s 15-year verification grand challenge. We believe that a suitable candidate for such a mini challenge is the development of a filesystem that is verifiably reliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.

We describe an extension of the SPIN model checker for use on multicore shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can, in some cases, be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multicore algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code and are compatible with most existing verification modes such as partial order reduction, the verification of temporal logic formulas, bitstate hashing, and hash-compact compression.

In this position statement, the author briefly describes how the software reliability problem has changed over the years, and the primary reasons for the recent creation of the Laboratory for Reliable Software at JPL.

Real-life bugs are successful because of their unfailing ability to adapt. In particular this applies to their ability to adapt to strategies that are meant to eradicate them as a species. Software bugs have some of these same traits. We will discuss these traits, and consider what we can do about them.

Software verification methods are used only sparingly in industrial software development today. The most successful methods are based on the use of model checking. There are, however, many hurdles to overcome before the use of model checking tools can truly become mainstream. To use a model checker, the user must first define a formal model of the application, and to do so requires specialized knowledge of both the application and of model checking techniques. For larger applications, the effort to manually construct a formal model can take a considerable investment of time and expertise, which can rarely be afforded. Worse, it is hard to secure that a manually constructed model can keep pace with the typical software application, as it evolves from the concept stage to the product stage. We describe a verification method that requires far less specialized knowledge in model construction. It allows us to extract models mechanically from source code. The model construction process now becomes easily repeatable, as the application itself continues to evolve. Once the model is constructed, existing model checking techniques allow us to perform all checks in a mechanical fashion, achieving nearly complete automation. The level of thoroughness that can be achieved with this new type of software testing is significantly greater than for conventional techniques. We report on the application of this method in the verification of the call processing software for a new telephone switch that was developed at Lucent Technologies.

How can we determine the added value of software verification techniques over the more readily available conventional testing techniques? Formal verification techniques introduce both added costs and potential benefits. Can we show objectively when the benefits will outweigh the cost?

A logic model checker can be an effective tool for debugging software applications. A stumbling block can be that model-checking tools expect the user to supply a formal statement of the correctness requirements to be checked in temporal logic. Expressing non-trivial requirements in logic, however, can be challenging. To address this problem, we developed a graphical tool, called the TimeLine Editor, that simplifies the formalization of certain kinds of requirements. A series of events and required system responses are placed on a timeline. The user converts the timeline specification automatically into a test automaton that can be used directly by a logic model checker or for traditional test-sequence generation. We have used the TimeLine Editor to verify the call processing code for Lucent's PathStar access server against the TelCordia LSSGR [LATA (local access and transport area) Switching Systems Generic Requirements] standards. The TimeLine Editor simplified the task of converting a large body of English prose requirements into formal, yet readable, logic requirements.

Formal verification methods are used only sparingly in software development.The most successful methods to date are based on the use of model checking tools.To use such tools, the user must first define a faithful abstraction of the application (the model), specify how the application interacts with its environment, and then formulate the properties that it should satisfy.Each step in this process can become an obstacle.To complete the verification process successfully often requires specialized knowledge of verification techniques and a considerable investment of time.In this paper we describe a verification method that requires little or no specialized knowledge in model construction.It allows us to extract models mechanically from the source of software applications, securing accuracy.Interface definitions and property specifications have meaningful defaults that can be adjusted when the checking process becomes more refined.All checks can be executed mechanically, even when the application itself continues to evolve.Compared to conventional software testing, the thoroughness of a check of this type is unprecedented.

Describes the design of VIP (Visual Interface for Promela), a graphical front-end to the model checker SPIN. VIP supports a visual formalism, called v-Promela, that connects the model checker to modern hierarchical notations for the specification of object-oriented, reactive systems. The formalism is comparable to formalisms such as UML-RT (Unified Modeling Language for Real-Time systems), ROOM (Real-time Object-Oriented Modeling) and Statecharts, but is presented in this paper in a framework that allows us to combine the benefits of a visual, hierarchical specification method with the power of LTL (linear temporal logic) model checking provided by SPIN. Like comparable formalisms, VIP can describe hierarchies of behaviour and of system structure. The formalism is designed to be transparent to the SPIN model checker itself, by allowing all central constructs to be translated mechanically into basic Promela, as already supported by the existing model checker.

It has become good practice to expect authors of new model checking algorithms to provide not only rigorous evidence of the algorithms correctness, but also evidence of their practical significance. Though the rules for determining what is and what is not a good proof of correctness are clear, no comparable rules are usually enforced for determining the soundness of the data that is used to support the claim for practical significance. We consider here how we can flag the more common types of omission. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

SPIN is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges. The paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications.

Abstract A traditional protocol implementation typically consists of at least two distinct parts, a sender and a receiver. Each part runs on a distinct machine, with the implementation provided by a local expert. At best, the two machines are of the same type and the protocol implementations are provided by the same person. More likely, however, the machines are not of the same type and the implementations of the two halves of the protocol are provided by two different people, working from an often loosely defined protocol specification. It seems almost unavoidable that the two implementations are not quite compatible. In this paper we consider an alternative technique. With this method, one of the two implementors can design, formally validate, and implement all the relevant protocol parts, including those parts that are to be executed remotely. Each communication channel is now terminated on the receiving side, by a single standard protocol interface, which can be called a universal asynchronous protocol interface, or UAPI. Though it is likely that the UAPI is most efficiently implemented in hardware, it can also trivially run as a software module, e.g. under a standard UNIX® operating system (in our case under 10th Edition Research Unix). This paper introduces the concept of a UAPI and explains how the sample software controller was constructed.

Abstract An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine (FSM) model of the system studied. The application of this method to systems of a practical size, though, is complicated by time and space requirements. If a system is larger, more space is needed to store the state descriptions and more time is needed to compare and analyze these states. This paper shows that if the FSM model is abandoned and replaced by a state vector model significant gains in performance are feasible, for the first time making it possible to perform effective validations of large systems.

Argos is a validation language for data communication protocols. To validate a protocol, a model in Argos is constructed consisting of a control flow specification and a formal description of the correctness requirements. This model can be compiled into a minimized lower level description that is based on a formal model of communicating finite state machines. An automated protocol validator trace uses these minimized descriptions to perform a partial symbolic execution of the protocol to establish its correctness for the given requirements.

This paper introduces a simple algebra for the validation of communication protocols in message passing systems. The behavior of each process participating in a communication is first modeled in a finite state machine. The symbol sequences that can be accepted by these machines are then expressed in "protocol expressions," which are defined as regular expressions extended with two new operators: division and multiplication. The interactions of the machines can be analyzed by combining protocol expressions via multiplication and algebraically manipulating the terms.