Component-based design and analysis: a case study

In this paper, we introduce a component-based design methodology and present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a well-known obstacle to system verification. In addition, the approach is illustrated by application to a non-trivial case study: the production cell. It is shown that not only the basic consistency property, viz. the freedom from unexpected reception and deadlock, but also other important safety properties in the design can be proved.