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
$\pi$-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.