Property specification, process verification, and reporting – A case study with vehicle-commissioning processes

• Our tool verifies if a given process for the commissioning of vehicles complies.
• Our approach supports the user-friendly specification and reporting of properties.
• We automatically generate properties through the instantiation of property templates.
• The developed transformation to Petri nets allows an automatic verification.
• Our tool is able to detect violations in large processes of the Audi AG.

Testing in the automotive industry is supposed to guarantee that vehicles are shipped without any flaw. Respective processes are complex, due to the variety of components and electronic devices in modern vehicles. To achieve error-free processes, their formal analysis is required. Specifying and maintaining properties the processes must satisfy in a user-friendly way is a core requirement on any verification system. We have observed that there are few property templates that testing processes must adhere to, and we describe these templates. They depend on the context of the processes, e.g., the components of the vehicle or testing stations. We have developed a framework that instantiates the templates of properties at verification time and then verifies the process against these instances. To allow an automatic verification we develop a transformation of the commissioning process to a Petri net. Using a novel approach, we are able to report the found violations to the user in a user-friendly way. Our empirical evaluation with the industrial partner has shown that our framework does detect property violations in processes. From expert interviews we conclude that our framework is user-friendly and well suited to operate in a real production environment.