The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.07 - July (1996 vol.22)
pp: 496-507
ABSTRACT
<p><b>Abstract</b>—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 <it>partial-order methods</it> 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 for a formal validation tool that has been used on several projects that are developing software for the Lucent Technologies 5ESS® 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.</p>
INDEX TERMS
Formal methods, automatic verification, validation, partial-order methods, concurrent programs, reachability analysis.
CITATION
Patrice Godefroid, Doron Peled, Mark Staskauskas, "Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs", IEEE Transactions on Software Engineering, vol.22, no. 7, pp. 496-507, July 1996, doi:10.1109/32.538606
5 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool