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

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

• FS95a: A. R. Flora-Holmquist , M. G. Staskauskas, Formal validation of virtual finite state machines, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.122, April 05-08, 1995
• FS95b: A. R. Flora-Holmquist, J. D. O'Grady and M. G. Staskauskas. Telecommunications software design using virtual finite state machines. In Proc. Intl. Switching Symposium (fSS'95), Berlin, Germany, April 1995.
• God94: Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department, November 1994. (Also available by anonymous ftp from ftp.montefiore.uIg.ac.be in the pub/po~package directory, file thesis.ps.Z).
• GP93: Patrice Godefroid , Didier Pirottin, Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract), Proceedings of the 5th International Conference on Computer Aided Verification, p.438-449, June 28-July 01, 1993
• Hol88: Gerard J. Holzmann, An improved protocol reachability analysis technique, Software—Practice & Experience, v.18 n.2, p.137-161, Feb., 1988 [doi>10.1002/spe.4380180203]
• KP92a: Shmuel Katz , Doron Peled, Defining conditional independence using collapses, Theoretical Computer Science, v.101 n.2, p.337-359, July 20, 1992 [doi>10.1016/0304-3975(92)90054-J]
• KP92b: Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992 [doi>10.1007/BF02252682]
• Ove81: William T. Overman, Verification of concurrent systems: function and timing, 1981
• Pel94: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• Val93: Antti Valmari, On-the-Fly Verification with Stubborn Sets, Proceedings of the 5th International Conference on Computer Aided Verification, p.397-408, June 28-July 01, 1993
• Wa92: F. Wagner. VFSM executable specification. Proc. CompEuro, 1992.
• WG93: Pierre Wolper , Patrice Godefroid, Partial-Order Methods for Temporal Verification, Proceedings of the 4th International Conference on Concurrency Theory, p.233-246, August 23-26, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools

General Terms:
Algorithms, Experimentation, Reliability, Verification