Verification and Validation of a model dedicated to mode handling of manufacturing systems

This paper focuses on verification and validation (V&V) of a model dedicated to mode handling of flexible manufacturing systems. This model, specified using the synchronous formalism Safe State Machines, was proposed in our earlier work. The rigorous semantics that characterize such formalism enable to provide formal verification mechanisms ensuring determinism and dependability. A structured framework for verification and validation of a specification model is presented. The main properties being verified are proposed and illustrated through an example of a manufacturing production cell. The formal analysis tools integrated into the development environment Esterel Studio are used within the design process.