Testing automation systems by means of model checking

Industrial automation systems are commonly obliged to comply with correctness requirements and safety standards. Testing and simulation are traditionally used to ensure this compliance. For mission-critical applications, formal verification and model checking in particular are also used, but such techniques are computationally intensive and difficult to apply in practice. This paper searches for synergies between testing and model checking by generalizing an earlier proposed formal test modeling framework. It presents a technique of testing automation systems with the use of model checking, which now supports multiple model checking environments and a more generic test case representation. The proposed technique is applied on a case study involving a simple safety-critical system with timing requirements. Experiments show that the technique is fast despite the use of formal methods and at the same time has several benefits compared to usual testing.