We propose a type-based resource usage analysis for the π-calculus
extended with resource creation/access primitives. The goal of the resource
usage analysis is to statically check that a program accesses resources such as
files and memory in a valid manner. Our type system is an extension of previous
behavioral type systems for the π-calculus, and can guarantee the safety
property that no invalid access is performed, as well as the property that
necessary accesses (such as the close operation for a file) are eventually
performed unless the program diverges. A sound type inference algorithm for the
type system is also developed to free the programmer from the burden of writing
complex type annotations. Based on the algorithm, we have implemented a
prototype resource usage analyzer for the π-calculus. To the authors'
knowledge, ours is the first type-based resource usage analysis that deals with
an expressive concurrent language like the pi-calculus