We have developed a formal validation tool that has been used on several projects that are developing software for AT&T's 5ESS™ telephone switching system. The tool uses Holzmann's supertrace algorithm to check for errors such as deadlock and livelock in networks of communicating processes. The validator invariably finds subtle errors that were missed during thorough simulation and testing; however, the brute-force search it performs can result in extremely long running times, which can be frustrating to users. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the running time of formal validation by avoiding redundant exploration of execution scenarios. In this paper, we describe the design of a partial-order algorithm for our validation tool and discuss its effectiveness. We show that a careful compile-time static analysis of process communication behavior yields information that can be used during validation to dramatically improve its performance. We demonstrate the effectiveness of our partial-order algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of 5ESS™ application domains, including call processing, signalling, and switch maintenance.

Numerous formal specification methods for reactive systems have been proposed in the literature. Because the significant differences between the methods are hard to determine, choosing the best method for a particular application can be difficult. We have applied several different methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL, and C, to an application problem encountered in the design of software for AT&T's 5ESS telephone switching system. We have developed a set of criteria for evaluating and comparing the different specification methods. We argue that the evaluation of a method must take into account not only academic concerns, but also the maturity of the method, its compatibility with the existing software development process and system execution environment, and its suitability for the chosen application domain.

Formal validation is a powerful technique for automatically checking that a collection of communicating processes is free from concurrency-related errors. Although validation tools invariably find subtle errors that were missed during thorough simulation and testing, the brute-force search they perform can result in excessive memory usage and extremely long running times. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the computational resources needed for formal validation by avoiding redundant exploration of execution scenarios. This paper investigates the behavior of partial-order methods in an industrial setting. We describe the design of a partial-order algorithm or a formal validation tool that has been used on several projects that are developing software for the Lucent Technologies 5ESS/sup (R/) telephone switching system. We demonstrate the effectiveness of the algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of 5ESS application domains.

Numerous formal specification methods for reactive systems have been proposed in the literature.Because the significant differences bet ween the methods are hard to determine, choosing the best method for a particular application can be difficult.We have applied several different methods, including Modechart, VFSM, ESTEREL, Basic LOTOS, Z, SDL and C, to an application problem encountered in the design of software for AT&T's 5ESS o telephone switching system.We have developed a set of criteria for evaluating and comparing the different specification methods.We argue that the evaluation of a method must take into account not only academic concerns, but also the maturity of the method, its compatibility with the existing software development process and system execution environment, and its suitability for the chosen application domain.

The formal derivation of an implementation of the I/O (input/output) subsystem portion of an existing operating system is presented. The I/O subsystem is responsible for allocating I/O resources such as tapes, disks, I/O channels in response to requests from user processes. The derivation employs the UNITY methodology which captures the concurrent interaction of the I/O subsystem with its environment. The verified resource allocation algorithm that results from the derivation has been used as part of a high-level design by software engineers implementing the I/O subsystem. As the largest application to date of the UNITY methodology, the derivation illustrates a number of techniques for organizing large specifications and proofs.>

The design of an electronic funds-transfer (EFT) system, using the UNITY parallel programming methodology, is presented. The process begins with a high-level specification that captures the essence of transaction processing in the system. In a series of refinement steps, this specification is transformed into one that leads directly to a program suitable for execution on the distributed architecture of the EFT system. Each refinement step involves replacing a data structure by a distributed version that can be implemented efficiently on the target architecture. By defining a correspondence between the replaced data structure and its distributed counterpart, it can be demonstrated formally that each refinement step preserves the intent of the original specification.>