Animating process-oriented formal descriptions: experiences and lessons

One way to describe a concurrent system is through a formal model that defines a temporal ordering on observable system events. Such models are typically structured as a hierarchy of processes, with process behaviour given in terms of events. The events represent system actions, including, in particular, communication with the system environment and internal inter-process communication. A number of specification languages have been developed to support this approach to system description. The mathematical nature of these notations and the conciseness of expression that they tend to encourage often leads to system specifications that are relatively difficult to understand. The purpose of this paper is to report on the experience gained and lessons learned from a series of projects whose broad objective has been to make such process-oriented specifications more accessible. Emphasis has been placed on supporting the specification developer but the techniques involved also aid communication with clients. All of the projects have used LOTOS (E. Brinksma, 1988) as the demonstration language