This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs
July 1996 (vol. 22 no. 7)
pp. 496-507

Abstract—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 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.

[1] A.R. Flora-Holmquist and M.G. Staskauskas, “Formal Validation of Virtual Finite State Machines,” Proc. Workshop Industrial-Strength Formal Specification Techniques (WIFT’95), pp. 122–129, Boca Raton, Fla. Apr. 1995.
[2] A.R. Flora-Holmquist, J.D. O'Grady, and M.G. Staskauskas, "Telecommunications Software Design Using Virtual Finite State Machines," Proc. Int'l Switching Symp. (ISS'95),Berlin, Germany, Apr. 1995.
[3] P. Godefroid, "Using Partial Orders to Improve Automatic Verification Methods," Proc. Second Int'l Workshop Computer-Aided Verification, pp. 176-185, 1990.
[4] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem, vol. 1032of Lecture Notes in Computer Science. Springer-Verlag, Jan. 1996.
[5] P. Godefroid and D. Pirottin, “Refining Dependencies Improves Partial-Order Verification Methods,” Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 438-449, June 1993.
[6] P. Godefroid and P. Wolper, "Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties," Formal Methods in System Design, pp. 149-164, Apr. 1993.
[7] P. Godefroid, D. Peled, and M. Staskauskas, "Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs," Proc. Int'l Symp. Software Testing and Analysis,San Diego, Calif., pp. 261-269, Jan. 1996.
[8] G.J. Holzmann, "An Improved Protocol Reachability Analysis Technique," Software, Practice and Experience, vol. 18, no. 2, pp. 137-161, 1988.
[9] S. Katz and D. Peled, "Defining Conditional Independence Using Collapses," Theoretical Computer Science, vol. 101, pp. 337-359, 1992.
[10] S. Katz and D. Peled, "Verification of Distributed Programs Using Representative Interleaving Sequences," Distributed Computing, vol. 6, pp. 107-120, 1992.
[11] W.T. Overman, "Verification of Concurrent Systems: Function and Timing," PhD thesis, Univ. of California, Los Angeles, 1981.
[12] D. Peled, "All from One, One for All: On Model Checking Using Representatives," Proc. Fifth Conf. Computer Aided Verification, vol. 697of Lecture Notes in Computer Science, Elounda, pp. 409-423. Springer-Verlag, June 1993.
[13] D. Peled, "Combining Partial Order Reductions with On-The-Fly Model-Checking," Formal Methods in System Design, vol. 8, pp. 39-64, 1996.
[14] A. Valmari, "Error Detection by Reduced Reachability Graph Generation," Proc. Ninth Int'l Conf. Application and Theory of Petri Nets,Venice, pp. 95-112, 1988.
[15] A. Valmari, "Heuristics for Lazy State Generation Speeds Up Analysis of Concurrent Systems," Proc. Finnish Artificial Intelligence Symp. STeP-88,Helsinki, vol. 2, pp. 640-650, 1988.
[16] A. Valmari, "A Stubborn Attack on State Explosion," Proc. Second Workshop Computer Aided Verification, vol. 531, Lecture Notes in Computer Science, pp. 156-165. Springer-Verlag, 1991.
[17] A. Valmari, "On-The-Fly Verification with Stubborn Sets," Proc. Fifth Conf. Computer Aided Verification, vol. 697of Lecture Notes in Computer Science, Elounda, pp. 397-408. Springer-Verlag, June 1993.
[18] F. Wagner, "VFSM Executable Specification," Proc. IEEE Int'l Conf. Computer System and Software Engineering, The Hague, pp. 226-231, 1992.
[19] P. Wolper and P. Godefroid, "Partial-Order Methods for Temporal Verification (invited paper)," Proc. CONCUR'93, vol. 715of Lecture Notes in Computer Science, Hildesheim, pp. 233-246. Springer-Verlag, Aug. 1993.

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
Usage of this product signifies your acceptance of the Terms of Use.