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.

References Powered by Scopus

Combining partial order reductions with on-the-fly model-checking

162Citations
N/AReaders
Get full text

Refining dependencies improves partial-order verification methods

94Citations
N/AReaders
Get full text

On-the-fly verification with stubborn sets

81Citations
N/AReaders
Get full text

Cited by Powered by Scopus

Counterexample-guided abstraction refinement for symbolic model checking

752Citations
N/AReaders
Get full text

Ten years of partial order reduction

102Citations
N/AReaders
Get full text

Verifying security protocols with Brutus

91Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

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

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 5

45%

Professor / Associate Prof. 4

36%

Lecturer / Post doc 1

9%

Researcher 1

9%

Readers' Discipline

Tooltip

Computer Science 7

70%

Philosophy 1

10%

Decision Sciences 1

10%

Engineering 1

10%

Save time finding and organizing research with Mendeley

Sign up for free