Using partial-order methods in the formal validation of industrial concurrent programs

24Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.

Abstract

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.

Cite

CITATION STYLE

APA

Godefroid, P., Peled, D., & Staskauskas, M. (1996). Using partial-order methods in the formal validation of industrial concurrent programs. In Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996 (pp. 261–269). Association for Computing Machinery, Inc. https://doi.org/10.1145/229000.226324

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free