How to Verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study

The formal verification of a real-time system requires either a proof theoretic or model theoretic approach. Both being applicable to a model of the proposed behaviour of the concurrent real-time system. This paper evaluates the use model checking and timed automata by their application to an adaptation of the Production Cell case study. The Uppaal tool is used in this evaluation. The modeling aspects were found to be straightforward, but to accomplish the necessary model checking required some knowledge of the underlying process. Nevertheless, the conclusion of the study is that these techniques are generally applicable and be can be undertaken in an engineering context without detailed domain knowledge of the model checking technique.