Refactoring design models for inductive verification

ABSTRACT

Systems composed of many identical processes can sometimes be verified inductively using a network invariant, but systems whose component processes vary in some systematic way are not amenable to direct application of that method. We describe how variations in behavior can be "factored out" into additional processes, thus enabling induction over the number of processes. The process is semi-automatic: The designer must choose from among a set of idiomatic transformations, but each transformation is applied and checked automatically.

REFERENCES

• 1: K R Apt , D C Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, v.22 n.6, p.307-309, May 30,1986 [doi>10.1016/0020-0190(86)90071-2]
• 2: Shing Chi Cheung , Jeff Kramer, Checking safety properties using compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.49-78, Jan. 1999 [doi>10.1145/295558.295570]
• 3: Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
• 4: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 5: R. P. Kurshan , K. L. McMillan, A structural induction theorem for processes, Information and Computation, v.117 n.1, p.1-11, Feb. 15, 1995 [doi>10.1006/inco.1995.1024]
• 6: E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997 [doi>10.1145/265943.265960]
• 7: Bo Sanden, Entity-life modeling and structured analysis in real-time software design—a comparison, Communications of the ACM, v.32 n.12, p.1458-1466, Dec. 1989 [doi>10.1145/76380.76386]
• 8: Antti Valmari , Ilkka Kokkarinen, Unbounded Verification Results by Finite-State Compositional Techniques: 10^any States and Beyond, Proceedings of the 1998 International Conference on Application of Concurrency to System Design, p.75, March 23-26, 1998
• 9: P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France
• 10: W. J. Yeh and M. Young. Re-designing tasking structure of ada programs for analysis:a case study. Software Testing, Verification, and Reliability, 4:223-253, 1994.

INDEX TERMS

Keywords:
compositional analysis, concurrency, network invariants, parameterized system, refactoring