Skip to main content

Über dieses Buch

The second half of the twentieth century has witnessed remarkable advances in technology. The unquestioned leader in this race has been computer technology. Even the most modest personal computers today have computing power that would have astounded the leading technol­ ogists a few decades earlier, and what's more, similar advances are pre­ dicted for many years to come. Looking towards the future, it has been conservatively estimated that in 2047 computers could easily be 100,000 times more powerful than they were in 1997 (Moore's law [Moore] would lead to an increase on the order of around 10 billion) [Bell]. Because of its enormous capability, computer technology is becoming pervasive across the technology spectrum. Nowadays it is not surpris­ ing to discover that very common household gadgets like your toaster contain computer technology. Televisions, microwave ovens, and even electric shavers contain software. And what's more, the use of computer technology has been estimated to double every two years [Gibbs]. In order to keep up with the growing technology demands and to fully utilize the ever more powerful computing platforms, software projects have become more and more ambitious. This has lead to software systems becoming dominant forces in system functionality. Further­ more, the ambition to realize significant portions of a system's function­ ality through software has extended into the high consequence realm. Presently, software controls many critical functions in (1) airplanes, (2) electronic commerce, (3) space-bound systems, (4) medical systems, and (5) various transportation systems such as automobiles and trains.



General Applications of Formal Methods and Systems


Chapter 1. Designware: Software Development by Refinement

This paper presents a mechanizable framework for software development by refinement. The framework is based on a category of higher-order specifications. The key idea is representing knowledge about programming concepts, such as algorithm design, datatype refinement, and expression simplification, by means of taxonomies of specifications and morphisms.
The framework is partially implemented in the research systems Specware, Designware, and Planware. Specware provides basic support for composing specifications and refinements via colimit, and for generating code via logic morphisms. Specware is intended to be general-purpose and has found use in industrial settings. Designware extends Specware with taxonomies of software design theories and support for constructing refinements from them. Planware builds on Designware to provide highly automated support for requirements acquisition and synthesis of high-performance scheduling algorithms.
Douglas R. Smith

Chapter 2. B: Towards Zero Defect Software

This paper introduces B, a mathematically based method and a computer based tool-kit for software engineering. The B-Method provides a notation and a method for the formal specification and design of software. Incremental construction of layered software as well as incremental mathematical verification have been guiding principles in its development. The method uses a ‘pseudo’ programming language Abstract Machine Notation as the language for design as well as for specification within the software process. AMN is based on an extension of Dijkstra’s guarded command language, with built-in structuring mechanisms for the construction of larger systems. The B-Method is explained in The B-Book [Abrial, 1997].The B-Toolkit supports the method over the spectrum of activities from specification through design and implementation into maintenance. The B-Toolkit comprises automatic and interactive theorem-proving assistants, and a set of software development tools: an AMN syntax & type checker, a specification animator and code generators, and promotes an object oriented approach at all stages of development. All tools are integrated into a window-based development environment. The B-Toolkit is developed and sold by B-Core.
Ib Sorensen, David Neilson

Chapter 3. The Use of B to Specify, Design and Verify Hardware

We have demonstrated that clocked synchronous logic can be developed within a formal software framework. The advantage of this approach is that it allows abstraction, animation and proof of refinement. The B-Toolkit supports these activities and has a VHDL generator. The validation tests can be agreed and carried out during animation early in the development cycle (a common technique in software). Proof of refinement may be important for critical applications. The AWE plans to explore the proof of their Arming System Processor with the techniques over-viewed in this paper.
Wilson Ifill, Ib Sorensen, Steve Schneider

Chapter 4. A System for Predictable Component-Based Software Construction

Large systems are invariably built from assembled components. It is essential for such systems to have predictable behavior, if the risks of failure are too high. To enable practical and modular verification of industrial-strength systems, software practitioners need to learn to build both behavioral specifications of components and component implementations that are annotated with suitable internal assertions. Neither of these tasks can be automated, in general. However, once suitable specifications and implementations of components are given, a mechanical system (with human assistance) can check in a modular and scalable fashion if component-based software behaves as specified. To illustrate the issues, the paper presents a non-trivial component-based example. The example underscores that predictable component-based construction is challenging, and that it cannot become practical, without educating students and software developers on principles of mathematical specifications and correct, efficient implementations.
M. Aronszajn, M. Sitaraman, S. Atkinson, G. Kulczycki

Chapter 5. Autonomous Decentralized Systems Technologies and Their Application to a Train Transport Operation System

Large, mission-critical systems are required to satisfy, as nearly as possible, a 100% availability requirement. This imposes an on-line property, which includes on-line expansion for constructing a system step-by-step without stopping the system’s operation, on-line maintenance for testing and repairing during the system operation, and fault-tolerance. Autonomous Decentralized Systems (ADS) have been proposed for achieving the on-line property, and its technologies have been effectively applied in various fields including transportation, factory automation, information service and so on.
ADS are realized by the Data Field (DF) architecture, where data is broadcast with the content code corresponding to the data attached. Each subsystem selects its data depending on the content code instead of the address. Subsystems independently start their execution after all of the necessary data is received. Based on the DF architecture, the on-line property is realized.
One of the applications of the ADS for the Tokyo Metropolitan-Area Train Transport Operation Control System is discussed here to show that the on-line property and the heterogeneous requirements for real-time control and high-throughput information services are achieved.
Kinji Mori

Case Study


Chapter 6. Bay Area Rapid Transit District Advance Automated Train Control System Case Study Description

This document contains an informal description of a portion of the Advanced Automatic Train Control (AATC) system being developed for the Bay Area Rapid Transit (BART) system. BART provides commuter rail service for part of California’s San Francisco bay area. Specifically, the informal specification given below focuses on those aspects of BART that are necessary to control the speed and acceleration for the trains in the system. Other aspects of BART control such as (1) communication error recovery, (2) routing (via switches) and (3) right-of-way signaling (via “gates”) are largely ignored. The scope of this case study is narrower than the AATC project as a whole, but within this narrowed scope, enough detail has been supplied to give a sense of the level of complexity involved.
Victor L. Winter, Raymond S. Berg, James T. Ringland

Chapter 7. Using SCR to Specify Requirements of the Bart Advanced Automated Train Control System

Since its introduction in 1978, the SCR (Software Cost Reduction) tabular notation has been used to represent the requirements of numerous safety-critical systems, including avionics systems, space systems, and control systems for nuclear plants. Our group has formulated a state-machine semantics for the SCR notation and a set of software tools for analyzing requirements specifications in the SCR tabular notation. To demonstrate the benefits of the SCR method for developing safety-critical systems, this chapter describes the application of SCR to a complex portion of the Advanced Automated Train Control (AATC) system under development for the Bay Area Rapid Transit (BART) system. Examples from an SCR specification of the required behavior of the AATC system are provided. The positive impact of applying our approach to the construction of the AATC system is summarized, and some important issues raised during the case study are discussed.
Constance Heitmeyer

Chapter 8. On the Construction of a Domain Language for a Class of Reactive Systems

A key step in the construction of high consequence software is its specification in a formal framework. In order to minimize the difficulty and potential for error, a specification should be expressed in a domain language supporting operators and structures that are intrinsic to the class of algorithms one wishes to specify.
In this paper we describe a language that is suitable for the algorithmic specification of software controllers for a class of reactive systems of which the Bay Area Rapid Transit (BART) system is an instance. We then specify an abstract controller for a subset of BART using this language.
Deepak Kapur, Victor L. Winter

Chapter 9. A Refinement-Based Approach to Deriving Train Controllers

The purpose of this paper is to demonstrate how transformation can be used to derive a high integrity implementation of a train controller from an algorithmic specification. The paper begins with a general discussion of high consequence systems (e.g., software systems) and describes how rewrite-based transformation systems can be used in the development of such systems. We then discuss how such transformations can be used to derive a high assurance controller for the Bay Area Rapid Transit (BART) system from an algorithmic specification.
Victor L. Winter, Deepak Kapur, Raymond S. Berg

Verification and Validation


Chapter 10. Systematic Validation of a Relational Control Program for the Bay Area Rapid Transit System

The failure of safety-critical systems, such as aircraft control systems, railway control systems, and nuclear power plant control systems, can cause catastrophic losses of life and property. Hence, it is imperative to assure the reliability and safety of these systems to a very high degree of confidence.
It is infeasible to perform this type of ultrahigh reliability analysis by treating the entire system as one unit. This paper develops an approach that combines relational programs with iterative enhancement. It allows a complex system to be divided into a series of increments such that each increment is decomposed into subsystems that can be independently assessed. An increment is related to the previous increment via transformations or clearly delineated enhancements that can be assessed independently. The subsystems are then automatically composed together to obtain the system.
The approach guarantees that the reliability and safety of the system can be inferred from the corresponding properties of the individual subsystems. It is illustrated using a case study drawn from the Bay Area Rapid Transit system project.
F. B. Bastani, V. Reddy, P. Srigiriraju, I.-L. Yen

Chapter 11. Verification of a Controller for Bart: An Approach Based on Horn Logic and Denotational Semantics

We present a semantics-based framework for verifying real-time con- trollers implemented in Ada. Our semantics-based framework uses techniques based on denotational semantics, logic programming, and partial evaluation. We illustrate our framework by verifying the correctness of the real-time controller for the Bay Area Rapid Transit System (BART). The main property we wish to verify is that if two consecutive trains start out with some minimum separation distance between them (that is deemed to be safe), then a safe distance is always maintained. This safe distance is dependent on a number of different variables, such as speed, acceleration, and track gradient. Our approach allows automatic derivation of a verification system from the Ada-implementation of the controller.
Lawrence King, Gopal Gupta, Enrico Pontelli

Chapter 12. Using Virtual Reality to Validate System Models

To date most validation techniques are highly biased towards calculations involving symbolic representations of problems. These calculations are either formal (in the case of consistency and completeness checks), or informal in the case of code inspections. We believe that an essential type of “evidence” of the correctness of the formalization process must be provided by (i.e., must originate from) human-based calculation. We further believe that human calculation can be significantly amplified by shifting from symbolic representations to graphical representations. This paper describes our preliminary efforts in realizing such a representational shift.
Victor L. Winter, Thomas P. Caudell


Weitere Informationen