Issue No. 07 - July (1996 vol. 22)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.538606
<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>
Formal methods, automatic verification, validation, partial-order methods, concurrent programs, reachability analysis.
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. , pp. 496-507, July 1996, doi:10.1109/32.538606