Behaviour Analysis for Validating Communication Patterns

The communication patterns of concurrent programs can be expressed succinctly using behaviours; these can be viewed as a kind of causal constraints or as a kind of process algebra terms. We present a system which infers behaviours from a useful fragment of Concurrent ML programs; it is based on previously developed theoretical results and forms the core of a system available on the Internet. By means of a case study, used as a benchmark in the literature, we shall see that the system facilitates the validation of certain safety conditions for reactive systems.