D. Thapa, C.M. Park, S.C. Park, and G.-N. Wang
Modelling, formal verification, simulation, t-MPSG (Message based part state graph), SMV (symbolic model verifier).
In this paper, we proposed an approach to formally model, and verify the shop floor controller logics. The verification process starts with modeling the targeted system using t-MPSG (an extended communicating finite state automaton). Thereafter, textual format of the t-MPSG is translated to native code of model checker, SMV. Afterwards, it can be combined with temporal logic to describe the required properties. Finally, model checking tool automatically verifies the model of the shop floor controller logic as per specified properties. In case of failure to satisfy the given properties, it produces counter examples. An illustration of the formal modeling and verification process is presented, in this paper, to clarify the approach, with a suitable example of shop floor control system.
Important Links:
Go Back
