Integrated Virtual Preparation and Commissioning: supporting formal methods during automation systems development

Virtual commissioning – the development and validation of industrial control systems against a simulation model – is attracting interest in the automotive industry. The main motivation for its use is that control systems can start to be integrated and tested before the construction of the physical system. In addition to this, the ability to continuously test can lead to increased reliability and enables better coping with late changes. At the same time, using formal methods during production preparation and control system design promise similar benefits. Formal methods however, are not seeing the same surge in interest – they are rarely used in the automotive industry. In this paper a framework is proposed, Integrated Virtual Preparation and Commissioning, where virtual commissioning models are used as a base for preparation and control system implementation assisted by formal methods. The extensive use of simulation in virtual commissioning allows computation results from formal methods to be continuously validated by visual inspection and using existing analysis tools (e.g. collision detection methods). The framework is applied in a case study, where the combination of a simulation model and a formal model is used as an aid in generating operation sequences for validation during production preparation. The resulting formal model can be used to study the behavior of the production system before a control system has been implemented