The Production Cell: an exercise in the formal verification of a UML model

We show how to model the Production Cell, a standard example for evaluating design notations for embedded systems, using the Unified Modelling Language (UML). Then, we use the vUML tool, developed by the authors, to verify our model of the Production Cell. The input model and the results from the verification are expressed using the UML notation, thus hiding the model checking formalism from the user. We also show how to use the object oriented decomposition of the model, that is given by a UML class diagram, to reduce the complexity of the model checking problem. We conclude that the vUML tool helps the designer to verify the software of distributed object oriented embedded systems, without learning all the details of a model checker.