1. A system for modeling behavior of a message-passing program module wherein the message-passing program module communicates with other program modules and wherein intended message-passing behavior of the message-passing program module is specified by a type annotation, the system comprising: typing rules defining a conformance relationship between the message-passing program module and the type annotation; and a type system applying a reasoning tool to the conformance relationship to render a conclusion on whether actions of the message-passing program module satisfy the intended behavior expressed by the type annotation.