Distributed message-passing based asynchronous systems are becoming increasingly important. Such systems are notoriously hard to design and test. A promising approach to help programmers design such programs is to provide a behavioral type system that checks for behavioral properties such as deadlock freedom using a combination of type inference and model checking. The fundamental challenge in making a behavioral type system work for realistic concurrent programs is state explosion. This paper develops the theory to design a behavioral module system that permits decomposing the type checking problem, saving exponential cost in the analysis. Unlike module systems for sequential programming languages, a behavioral specification for a module typically assumes that the module operates in an appropriate concurrent context. We identify assume-guarantee reasoning as a fundamental principle in designing such a module system. Concretely, we propose a behavioral module system for π-calculus programs. Types are CCS processes that correctly approximate the behavior of programs, and by applying model checking techniques to process types one can check many interesting program properties, including deadlock-freedom and communication progress. We show that modularity can be achieved in our type system by applying circular assume-guarantee reasoning principles whose soundness requires an induction over time. We state and prove an assume-guarantee rule for CCS. Our module system integrates this assume-guarantee rule into our behavioral type system.
展开▼
