Verification of complex systems using incremental operational specifications
| Autor: | Bruce Robert Wieand, Cheron Vail, David Nesbitt, William E. Howden |
|---|---|
| Rok vydání: | 1991 |
| Předmět: |
Information Systems and Management
Computer science business.industry Distributed computing Principal (computer security) Avionics COBOL Functional description Computer Science Applications Theoretical Computer Science Consistency (database systems) Software Artificial Intelligence Control and Systems Engineering Formal specification Information system Graph (abstract data type) business computer Algorithm computer.programming_language |
| Zdroj: | Information Sciences. :427-450 |
| ISSN: | 0020-0255 |
| DOI: | 10.1016/0020-0255(91)90092-9 |
| Popis: | The principal technological problem in large systems development and maintenance is the management of complexity. Part of the problem is that there is seldom a complete set of formal specifications for such systems. This may not change for a variety of reasons. Such systems are often transaction oriented, and there is no concise functional description of their behavior. The code itself is the only detailed, complete description. In addition, during the development of such systems, the functional and design specifications evolve, and required properties of one part of the system become known at intermediate points in the development of some other part. An approach to this problem is described which depends on the use of operational specifications. It is based on studies of faults occurring in large systems, and an investigation of the ways in which humans make errors. The approach assumes that the information available about a large system usually consists of the program plus additional operational information in the form of incremental specifications . The program itself is considered to be an operational description in which sequences of operations are described using a graph. The additional operational information consists of partial ordering information about those operations. It also allows the user, for example, to note at one point in the graph that it is expected that some operation has been performed at earlier points. This leads to the consideration of the different states that can occur at some program location, where the states are defined either directly or indirectly in terms of operations occurring before or after that location. In order to make analysis tractable, incremental specifications are limited to constructs producing only a finite number of possible states. Verification of a system consists of determining the consistency of its operational specifications. Several incremental specifications analyzers have been constructed. The first was built for analyzing COBOL programs, and contained a variety of other interesting features such as a symbolic evaluation capability for detecting infeasible paths. Two others have been constructed for analyzing the code in a real-time avionics system. These are described, including one called QDA2 which has been used to detect the occurrence of errors in a heavily tested piece of flight software. All of the experiments with these analyzers confirm that they are easy to use, and effective in discovering the presence of an pervasive and important class of errors in large systems which have been characterized as “decomposition errors.” The basic features of our latest analyzer, QDAA, designed for detecting faults in ADA programs are also described. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|