Formal specification and analysis of production systems

This paper discusses how formal methods can be integrated with existing simulation techniques to specify and analyse production systems. Simulation is very well suited for performance analysis of production systems, such as cycle time or throughput approximations. However, it fails with respect to behavioural analysis of these systems, such as deadlock and livelock detection. Formal methods are mathematical notations and techniques especially designed for behavioural analysis. We show that it is possible to integrate a particular formal methods technique, called model checking, with existing simulation based techniques. The resulting mix provides powerful tools to analyse both performance and behavioural properties of production systems, which will be shown by two examples.