Types as models: model checking message-passing programs

ABSTRACT

Abstraction and composition are the fundamental issues in making model checking viable for software. This paper proposes new techniques for automating abstraction and decomposition using source level type information provided by the programmer. Our system includes two novel components to achieve this end: (1) a behavioral type-and-effect system for the π-calculus, which extracts sound models as types, and (2) an assume-guarantee proof rule for carrying out compositional model checking on the types. Open simulation between CCS processes is used as both the subtyping relation in the type system and the abstraction relation for compositional model checking.We have implemented these ideas in a tool---PIPER. PIPER exploits type signatures provided by the programmer to partition the model checking problem, and emit model checking obligations that are discharged using the SPIN model checker. We present the details on applying PIPER on two examples: (1) the SIS standard for managing trouble tickets across multiple organizations and (2) a file reader from the pipelined implementation of a web server.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993 [doi>10.1145/151646.151649]
• 2: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 3: Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.207, July 27-30, 1996
• 4: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 5: T. Anitoft, F.Nielson, and H.R. Nielson. Type and Effect Systems. Behaviours for Concurrency. Imperial College Press, 1999.
• 6: S. Chaki, S.K. Rajaniani, and J. Rehof. Types as models: Model checking niessage-passing programs. Technical report, Microsoft Research, 2001. Available at research.microsoft, com/behave.
• 7: S. Christensen, Y. Hirshfeld, and F. Moiler. Decidable subsets of CCS. The Computer Journal, 37(4):233-242, 1994.
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: Customer Support Consortium (CSC) and Desktop Management Task Force (DMTF). Service incident standard (sis) specification, version 1.1. Technical report, DMTF. Available at WWW. dmtf. org.
• 10: Ásgeir Th. Eiríksson, The Formal Design of 1M-gate ASICs, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.49-63, November 04-06, 1998
• 11: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 12: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 13: A. Gordon and A. Jeffrey. Typing corresondence assertions for communication protocols. In MFPS: Mathematical Foundations of Programming Semantics, pages 99 120. BRICS Notes Series NS-01-2, 2001. T. A. Henzinger, X. Liu, S. Qadeer, and S. K.
• 14: Thomas A. Henzinger , Xiaojun Liu , Shaz Qadeer , Sriram K. Rajamani, Formal specification and verification of a dataflow processor array, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.494-499, November 07-11, 1999, San Jose, California, United States
• 15: Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, An Assume-Guarantee Rule for Checking Simulation, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.421-432, November 04-06, 1998
• 16: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 17: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 18: Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
• 19: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-141, January 2001, London, United Kingdom
• 20: Kim G. Larsen , Robin Milner, A compositional protocol verification using relativized bisimulation, Information and Computation, v.99 n.1, p.80-108, July 1992 [doi>10.1016/0890-5401(92)90025-B]
• 21: J. R. Larus and M. Parkes. Using cohort scheduling to enhance server performance. Technical Report MSR-TR-2001-39, Microsoft Research, 2001.
• 22: Kenneth L. McMillan, A Compositional Rule for Hardware Design Refinement, Proceedings of the 9th International Conference on Computer Aided Verification, p.24-35, June 22-25, 1997
• 23: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 24: J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417-426, 1981.
• 25: Hanne Riis Nielson , Flemming Nielson, Higher-order concurrent programs with finite communication topology (extended abstract), Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.84-97, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174538]
• 26: Franz Puntigam , Christof Peter, Changeable interfaces and promised messages for concurrent components, Proceedings of the 1999 ACM symposium on Applied computing, p.141-145, February 28-March 02, 1999, San Antonio, Texas, United States [doi>10.1145/298151.298223]
• 27: Sriram K. Rajamani , Jakob Rehof, A Behavioral Module System for the Pi-Calculus, Proceedings of the 8th International Symposium on Static Analysis, p.375-394, July 16-18, 2001
• 28: António Ravara , Vasco Thudichum Vasconcelos, Typing Non-uniform Concurrent Objects, Proceedings of the 11th International Conference on Concurrency Theory, p.474-488, August 22-25, 2000
• 29: Davide Sangiorgi, &pgr;-calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, v.167 n.1-2, p.235-274, Oct. 30, 1996
• 30: Davide Sangiorgi, A theory of bisimulation for the &lgr;-calculus, Acta Informatica, v.33 n.1, p.69-97, 1996 [doi>10.1007/s002360050036]
• 31: Nobuko Yoshida, Graph Types for Monadic Mobile Processes, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, p.371-386, December 18-20, 1996