Model-based design of concurrent programs

A model is a simplified representation of the real world and, as such, includes only those aspects of the real-world system relevant to the problem at hand. The paper reviews a modelling approach to the design of concurrent programs in which models represent the behaviour of concurrent Java programs. A notation based on CSP is used to model behaviour. Tool support enables both interactive model exploration and the mechanical verification of required safety and liveness properties. Models are systematically translated into Java programs. The approach, supported by a textbook, forms the basis of a course at the authors' institution-and has also been widely adopted elsewhere. With the benefit of five years hindsight, we examine the strengths and weaknesses of the approach and look at some of the subsequent remedies and directions.