Writing requirements in a formal notation permits automatic assessment of such properties as ambiguity, consistency, and completeness. However, verifying that the properties expressed in requirements are preserved in other software life cycle artifacts remains difficult. The existing techniques either require substantial manual effort and skill or suffer from exponential explosion of the number of states in the generated state spaces. "Light-weight" formal methods is an approach to achieve scalability in fully automatic verification by checking an abstraction of the system for only certain properties. We describe light-weight techniques for automatic analysis of consistency between software requirements (expressed in SCR) and detailed designs in low-degree-polynomial time, achieved at the expense of using imprecise data-flow analysis techniques. A specification language SCR describes the systems as state machines with event-driven transitions. We define detailed designs to be consistent with their SCR requirements if they contain exactly the same transitions. We have developed a language for specifying detailed designs, an analysis technique to create a model of a design through data-flow analysis of the language constructs, and a method to automatically generate and check properties derived from requirements to ensure a design's consistency with them. These ideas are implemented in a tool named CORD, which we used to uncover errors in designs of some existing systems.

Requirements of event-based systems can be automatically analyzed to determine if certain safety properties hold. However, we lack comparable methods to verify that implementations maintain the properties guaranteed by the requirements. We have built a tool that compares implementations written in C with their requirements. Requirements describe events which cause state transitions. Implementations are annotated to describe changes in the values of their requirement's variables, and dataflow analysis techniques are used to determine the set of events which cause particular state changes. To show that an implementation is consistent with its requirements, we show that each event causing a change of state in the implementation appears in the requirements, and that all the events specified to cause state changes in the requirements appear in the implementation. The annotation language encourages programmers to describe local program behaviors. These behaviors are collected into system-level behaviors, which are compared to those in the requirements. Since our analysis is not based on program code, annotations can describe behaviors at any level of granularity. We illustrate the use of our tool with several different annotations of a temperature-control system.

This paper describes a uniform approach to the automation of verification tasks associated with while statements, representation functions for abstract data types, generic program units, and abstract base classes. Program units are annotated with equations containing symbols defined by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and sufficient completeness. Sets of axioms are developed by stepwise extensions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural induction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductive arguments and providing hints for necessary lemmas, without which formal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain.>

Software errors frequently arise from incorrect system requirements. Successful requirements acquisition requires a thorough review process in which both domain experts and implementers can participate. Research groups [6, 10] have developed notations with precise meanings that can be read by both groups of reviewers. In [3], we showed how such requirements, in particular Software Cost Reduction (SCR) requirements, could be analyzed with formal methods. We developed methods for detailing SCR tabular requirements (with information that appears elsewhere in the SCR requirements document), translating the detailed requirements into a finite state machine (representing the system's global reachability graph), and proving safety assertions with a model checker for branching-time temporal logic. In this paper

It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system.>

Exception handling mechanisms were added to programming languages to segregate normal algorithmic processing from error processing. However, handlers which are typically associated with exceptions through a program's control features, clutter source text when features are nested or when different objects require different responses to exceptions. The authors describe a method for associating handlers with data objects in declarations that better segregates algorithmic and error processing. They call their notion data-oriented exception handling to distinguish it from more conventional, control-oriented mechanisms. Empirical studies of Ada programs indicate that conventional exception handling mechanisms are more complex than necessary and that data-oriented exception handling can be used to produce programs that are smaller, better structured, and easier to understand and modify.>

An introductory computer science course is developed, much as calculus is a basic course for mathematics and the physical sciences, concerned primarily with theoretical foundations and methodology rather than apprenticeship through applications. In this work, the principles taught in the course are described and an example illustrating them is given.>

Because large-scale software development is a struggle against internal program complexity, the modules into which programs are divided play a central role in software engineering. A module encapsulating a data type allows the programmer to ignore both the details of its operations, and of its value representations. It is a primary strength of program proving that as modules divide a program, making it easier to understand, so do they divide its proof. Each module can be verified in isolation, then its internal details ignored in a proof of its use. This paper describes proofs of module abstractions based on functional semantics, and contrasts this with the Alphard formalism based on Hoare logic.

Remote procedure call (RPC) is a programming primitive that makes building distributed programs easier. Atomicity, whkh implies totality and serializability, has been recognized as an important property to assure consistency in spite of computing node crashes. We have implemented an atomk remote procedure call mechanism which provides users a simple and reliable language primitive. Concurrency is controlled by attaching a call graph path identifier to each message representing a procedure call. Procedures keep their last accepted calling message paths to compare against incoming message paths. Only calls that can be serialized are accepted. Associated states of static variables are saved in backup processors on procedure entry and restored to corresponding variables in case of procedure crash. Detailed concurrency control and recovery algorithms are given, and illustrated with examples.

This paper describes our experience specifying, implementing, and validating a record-oriented text editor similar to one discussed in [7]. Algebraic axioms served as the specification notation; and the implementation was tested with a compiler-based system that uses the axioms to test implementations with a finite collection of test cases. Formal specifications were sometimes difficult to produce, but helped reveal errors during unit testing. Thorough exercising of the implementations by the specifications resulted in few errors persisting until integration.

Abstract DAISTS (Data Abstraction Implementation, Specification and Testing System)1 is a compiler tool‐base for program development. The compiler combines an automated ‘oracle’, which checks consistency conditions derived from algebraic specifications of modules, with run‐time routines that judge the quality of a user's test data according to statement and expression coverage criteria. This paper describes some of the implementation techniques used in DAISTS.

A compiler-based system DAISTS that combines a data-abstraction implementation language (derived from the SIMULA class) with specification by algebraic axioms is described.The compiler, presented with two independent syntactic objects in the axioms and implementing code, compiles a "program" that consists of the former as test driver for the latter.Data points, in the form of expressions using the abstract functions and constant values, are fed to this program to determine if the implementation and axioms agree.Along the way, structural testing measures can be applied to both code and axioms to evaluate the test data.Although a successful test does not conclusively demonstrate the consistency of axioms and code, in practice the tests are seldom successful, revealing errors.The advantage over conventional programming systems is threefold:(1) The presence of the axioms eliminates the need for a test oracle; only inputs need be supplied.(2) Testing is automated: a user writes axioms, implementation, and test points; the system writes the test drivers.(3) The results of tests are often surprising and helpful because it is difficult to get away with "trivial" tests: what is not significant for the code is liable to be a severe test of the axioms, and vice versa.

Abstract This paper describes SIMPL‐D, a stack‐based language with data abstraction features, and some of the details of its implementation. The language allows users to define new types that are parameterized by size and to perform system‐defined operations (e.g. assignment) on objects with user‐defined types. The use of object‐describing templates in the implementation of storage allocation, assignment and returning values from functions is discussed. Finally, the conflicts between automatic initialization and separate compilation are explained.

The language in which programs are written can have a substantial effect on their reliability. This paper discusses the design of programming languages to enhance reliability. It presents several general design principles, and then applies them to particular languages constructs. Since the validity of such design principles cannot be logically proved, empirical evidence is needed to support or discredit them. A major experiment to measure the effect of nine specific language-design decisions in one context has been performed. Analysis of the frequency and persistence of errors shows that several decisions had a significant impact on reliability.