No.050 Software Contracts for Communication, Monitoring, and Security

Communication contracts describe the global interactive behaviour of
concurrent and distributed systems. The challenge is to verify whether
a given program (or collection of programs) adheres a contract. If
that turns out to be the case, properties such as absence of 'message
not understood', undesired races and deadlocks are automatically
guaranteed. We show one such system for Message Passing Interface
programs.