A new method for FMS modeling and formal verification

Flexible Manufacturing System (FMS) is a complex asynchronous concurrent system. The model of FMS should have the abilities to express the concurrency in the system and to analyze the behavior of the system. It is difficult to use any one method to model such a complex system as FMS. A modeling and verifying method using object-oriented modeling language "Unified Modeling Language (UML)" and SPIN (PROMELA model) is presented in this paper. Class diagram in UML is used to represent the static relations among the objects in FMS, and state diagram is used to describe the dynamic behaviour of the system. Then the UML model is translated into PROMELA model automatically, and property checking is followed with SPIN which is a model checking tools. The method can describe and check the properties of the system (from modeling, simulation, to model checking), and can be used to design reliable FMS control software naturally.