Aircraft automation designers are faced with the challenge to develop and improve automation such that it is transparent to the pilots using it. To identify problems that may arise between pilots and automation, methods are needed that can uncover potential problems with automation early in the design process. In this paper, simulation and model checking are combined and their respective advantages leveraged to find problematic human-automation interaction using methods that would be available early in the design process. A particular problem of interest is automation surprises, which describe events when pilots are surprised by the actions of the automation. The Tarom flight 381 incident involving the former Airbus automatic speed protection logic, leading to an automation surprise, is used as a common case study. Results of this case study indicate that both methods identified the automation surprise found in the Tarom flight 381 incident, and that the simulation identified additional automation surprises associated with that flight logic. The work shows that the methods can be symbiotically combined, and the joint method is suitable to identify problematic human-automation interaction such as automation surprise.

To identify problems that may arise between pilots and automation, methods are needed that can uncover potential problems with automation early in the design process. Such potential problems include automation surprises, which describe events when pilots are surprised by the actions of the automation. In this work, agent-based, hybrid time simulation and model checking are combined and their respective advantages leveraged in an original manner to find problematic human-automation interaction (HAI) early in the design process. The Tarom 381 incident involving the former Airbus automatic speed protection logic, leading to an automation surprise, was used as a common case study for both methodology validation and further analysis. Results of this case study show why model checking alone has difficulty analyzing such systems and how the incorporation of simulation can be used in a complementary fashion. The results indicate that the method is suitable to examine problematic HAI, such as automation surprises, allowing automation designers to improve their design.

We outline the current approach to certification of aircraft software, and the role of DO-178B. We consider evidence for its effectiveness and discuss possible explanations for this. We then describe how changes in aircraft systems and in the air traffic system pose new challenges for certification, chiefly by increasing the extent of interaction and integration.

Breakdowns in complex systems often occur as a result of system elements interacting in ways unanticipated by analysts or designers. The use of task behavior as part of a larger, formal system model is potentially useful for analyzing such problems because it allows the ramifications of different human behaviors to be verified in relation to other aspects of the system. A component of task behavior largely overlooked to date is the role of human-human interaction, particularly human-human communication in complex human-computer systems. We are developing a multi-method approach based on extending the Enhanced Operator Function Model language to address human agent communications (EOFMC). This approach includes analyses via theorem proving and future support for model checking linked through the EOFMC top level XML description. Herein, we consider an aviation scenario in which an air traffic controller needs a flight crew to change the heading for spacing. Although this example, at first glance, seems to be one simple task, on closer inspection we find that it involves local human-human communication, remote human-human communication, multi-party communications, communication protocols, and human-automation interaction. We show how all these varied communications can be handled within the context of EOFMC.

Littlewood introduced the idea that software may be possibly perfect and that we can contemplate its probability of (im)perfection. We review this idea and show how it provides a bridge between correctness, which is the goal of software verification (and especially formal verification), and the probabilistic properties such as reliability that are the targets for system-level assurance. We enumerate the hazards to formal verification, consider how each of these may be countered, and propose relative weightings that an assessor may employ in assigning a probability of perfection.

The early 1980s saw the development of some rather sophisticated distributed systems. These were not merely networked file systems: rather, using remote procedure calls, hierarchical naming, and what would now be called middleware, they allowed a collection of systems to operate as a coherent whole. One such system in particular was developed at Newcastle that allowed pre-existing applications and (Unix) systems to be used, completely unchanged, as components of an apparently standard large (multiprocessor) Unix system. The distributed secure system (DSS) described in our 1983 paper proposed a new way to construct secure systems by exploiting the design freedom created by this form of distributed computing. The DSS separated the security concerns of policy enforcement from those due to resource sharing and used a variety of mechanisms (dedicated components, cryptography, periods processing, separation kernels) to manage resource sharing in ways that were simpler than before. In this retrospective, we provide the full original text of our DSS paper, prefaced by an introductory discussion of the DSS in the context of its time, and followed by an account of the subsequent implementation and deployment of an industrial prototype of DSS, and a description of its modern interpretation in the form of the MILS architecture. We conclude by outlining current opportunities and challenges presented by this approach to security.

Traditional, standards-based approaches to certification are hugely expensive, of questionable credibility when development is outsourced, and a barrier to innovation. This paper is a call and a manifesto for new approaches to certification. We start by advocating a goal-based approach in which unconditional claims delivered by formal methods are combined with other evidence in multi-legged cases supported by Bayesian analysis. We then describe the necessity, and the challenge, of extending this to compositional certification and outline promising directions for accomplishing this. Finally, we consider the provocative possibility of adaptive systems in which methods of analysis traditionally used to support certification at design time are instead used for synthesis and monitoring at runtime, and certification is performed "just-in-time."

The world at large cares little for verified software; what it cares about are trustworthy and cost-effective systems that do their jobs well. We examine the value of verified software and of verification technology in the systems context from two perspectives, one analytic, the other synthetic. We propose some research opportunities that could enhance the contribution of the verified software initiative to the practices of systems engineering and assurance.

Technological innovations are sweeping through the field of formal verification. These changes are disruptive to tools based on interactive theorem proving, which needs new ways to integrate the capabilities of novel technologies. I describe two approaches. One is development and use of SMT solvers: these use techniques from theorem proving but apply them in ways that enable model checking, while also supporting highly automated theorem proving. The other is a proposal for an evidential tool bus: a loosely coupled architecture that allows many different verification components to collaborate to solve problems beyond the capability of any single component

This full-day tutorial provides an introduction to automated formal methods using modern tools and methods. PVS is a comprehensive system for formal specification and analysis. It provides an attractive specification language based on higher order logic extended with dependent types and structural and predicate subtypes, and includes constructs for recursively defined abstract data types, recursive functions, inductive relations, and tabular specifications, as well as traditional logical formulas. Analysis capabilities include very strong typechecking (which can involve theorem proving), direct execution (at speeds within a factor of five of hand-crafted C), random testing, theorem proving, and symbolic model checking (with predicate abstraction). The PVS theorem prover provides powerful automation including rewriting and decision procedures for real and integer arithmetic, and is scriptable. Properties to be verified can be expressed as individual logical formulas, as CTL properties (for model checking), or as theory interpretations. The system is supported by massive built-in and user-provided libraries of specifications for mathematics and computer science.

The increasing performance of modern model-checking tools offers high potential for the computer-aided design of fault-tolerant algorithms. Instead of relying on human imagination to generate taxing failure scenarios to probe a fault-tolerant algorithm during development, we define the fault behavior of a faulty process at its interfaces to the remaining system and use model checking to automatically examine all possible failure scenarios. We call this approach "exhaustive fault simulation". In this paper we illustrate exhaustive fault simulation using a new startup algorithm for the time-triggered architecture (TTA) and show that this approach is fast enough to be deployed in the design loop. We use the SAL toolset from SRI for our experiments and describe an approach to modeling and analyzing fault-tolerant algorithms that exploits the capabilities of tools such as this.

Embedded control systems typically comprise continuous control laws combined with discrete mode logic. These systems are modeled using a hybrid automaton formalism, which is obtained by combining the discrete transition system formalism with continuous dynamical systems. This paper develops automated analysis techniques for asserting correctness of hybrid system designs. Our approach is based on symbolic representation of the state space of the system using mathematical formulas in an appropriate logic. Such formulas are manipulated using symbolic theorem proving techniques. It is important that formal analysis should be unobtrusive and acceptable to engineering practice. We motivate a methodology called invisible formal methods that provides a graded sequence of formal analysis technologies ranging from extended typechecking, through approximation and abstraction, to model checking and theorem proving. As an instance of invisible formal methods, we describe techniques to check inductive invariants, or extended types, for hybrid systems and compute discrete finite state abstractions automatically to perform reachability set computation. The abstract system is sound with respect to the formal semantics of hybrid automata. We also discuss techniques for performing analysis on nonstandard semantics of hybrid automata. We also briefly discuss the problem of translating models in Simulink/Stateflow language, which is widely used in practice, into the modeling formalisms, like hybrid automata, for which analysis tools are being developed.

This paper shows that deterministic consensus in synchronous distributed systems with link faults is possible, despite the impossibility result of Gray (1978). Instead of using randomization, we overcome this impossibility by moderately restricting the inconsistency that link faults may cause system-wide. Relying upon a novel hybrid fault model that provides different classes of faults for both nodes and links, we provide a formally verified proof that the m+1-round Byzantine agreement algorithm OMH (Lincoln and Rushby (1993)) requires n > 2f/sub l//sup s/ + f/sub l//sup r/ + f/sub l//sup ra/ + 2(f/sub a/ + f/sub s/) + f/sub o/ + f/sub m/ + m nodes for transparently masking at most f/sub l//sup s/ broadcast and f/sub l//sup r/ receive link faults (including at most f/sub l//sup ra/ arbitrary ones) per node in each round, in addition to at most f/sub a/, f/sub s/, f/sub o/, f/sub m/ arbitrary, symmetric, omission, and manifest node faults, provided that m /spl ges/ f/sub a/ + f/sub o/ + 1. Our approach to modeling link faults is justified by a number of theoretical results, which include tight lower bounds for the required number of nodes and an analysis of the assumption coverage in systems where links fail independently with some probability p.

Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system and, then, to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems.

Ubiquitous abstraction involves the construction of many different abstracted system descriptions at many different points in an analysis, and for several different purposes. This method has great promise as a way to ease difficulties and increase productivity and automation in the formal analysis of concurrent systems. The approach also provides a new way to combine different tools, such as theorem provers and model checkers, though full exploitation of this opportunity requires modification to the tools so that they can exchange symbolic values (e.g. the reachable state set, or a counterexample) rather than merely report the success or failure of their own local analysis. Some of the capabilities described are already integrated in a system called InVeSt (S. Bensalem et al., 1998) and initial experiments with this and other prototypes developed as part of our "Symbolic Analysis Laboratory" (SAL) are quite promising.

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.

Formal methods have gained acceptance in the hardware field through a pragmatic approach that has succeeded in providing systematic, scalable, highly automated, and cost effective treatments for certain stereotypical problems of practical importance. By identifying stereotypical problems, the effort required to develop effective formal methods has been amortized over many applications. We suggest that formal methods can achieve similar industrial success in selected software applications by following the same principles. As an illustration, we examine approaches to the stereotypical problem of interpreter correctness in the presence of timing differences between the specification and implementation interpreters. In hardware, this corresponds to the problem of verifying microprogrammed, pipelined, or superscalar processors, but it has wider applications to any system-hardware or software-that can be considered as an interpreter.

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model "reliable computing platform" (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5. Several of the formal specifications and verifications performed in support of RCP and AAMP5 are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification. We outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications.>

A small modification to the interactive convergence clock synchronization algorithm allows it to tolerate a larger number of simple faults than the standard algorithm, without reducing its ability to tolerate arbitrary or "Byzantine" faults.Because the extended caseanalysis required by the new fault model complicates the already intricate argument for correctness of the algorithm, it has been subjected to mechanically-checked formal verification.The fault model examined is similar to the "hybrid" one previously used for the problem of distributed consensus: in addition to arbitrary faults, we also admit symmetr~c (i.e., consistent) and manifest (i.e., detect able) faults.With n processors, the modified algo-"

The authors describe their experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized.>

We describe the design of a distributed general-purpose computing system that enforces a multilevel security policy. The system is composed of standard UNIX systems and small trustworthy security mechanisms linked together in such a way as to provide a total system which, is not only demonstrably secure, but also highly efficient and cost effective. Despite the heterogeneity of its components, the system as a whole appears to be a single multilevel secure UNIX system, since the fact that it is actually a distributed system is completely hidden from its users and their programs.This is achieved through the use of the "Newcastle Connection", a software subsystem that links together multiple UNIX or UNIX-look-alike systems, without requiring any changes to the source code of either the operating system or any user programs. Construction of a prototype implementation is in progress.

This paper reviews some of the difficulties that arise in the verification of kernelized secure systems and suggests new techniques for their resolution.