Model Checking Plans for Flexible Manufacturing Systems
| Authors: | Dias da Silva Leandro, Federal University of Campina Grande, Brazil
Almeida Hyggo, Federal University of Campina Grande, Brazil
Perkusich Angelo, Federal University of Campina Grande, Brazil
Rezende Barros Péricles, Federal University of Campina Grande, Brazil |
|---|
| Topic: | 5.2 Manufacturing Modelling for Management and Control |
|---|
| Session: | Manufacturing Modelling, Management and Control |
|---|
| Keywords: | Manufacturing Systems, Planning, Model Checking, Colored Petri Nets |
|---|
Abstract
In this work an approach to analyze non-deterministic executionplans for flexible manufacturing systems is presented. Thisapproach consists of modeling the system using coloured Petri netsand then, by simulation, discover the possible executions for thesystem. After, model checking is used to prove that the modelbehavior do not deviate from the planning. Based on this approachit is possible to model a production system based on cells and topredict and to prove its behavior before the system is developed.Therefore, the analyzed model can be used to develop flexible anddependable production systems to meet the market requirements ofquantity, diversity, and quality.
