Formal modeling and verifying of FMS

A modeling method for controller in FMS is presented. This method is based upon the timed automata. Model checker tool UPPAAL is used to model, simulate and verify the FMS model. In the previous work about FMS modeling, the behavior of FMS is more emphasized than the performance, or vice versa. Because the time is included into the modeling method in this paper, the scheduling and controlling problems in FMS can be integrated into this model. The performance of the system can be guaranteed while the system behavior is controlled. Upon this model, the optimal scheduling and optimal controlling can also be checked and verified.