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

作者:

Highlights:

• 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.

摘要

Highlights•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.

论文关键词:Property specification,Business process management,Workflow management,Verification,Model checking,Petri net,Industrial processes,Vehicle commissioning processes

论文评审过程:Received 28 November 2014, Revised 27 August 2015, Accepted 7 September 2015, Available online 26 September 2015, Version of Record 8 December 2015.

论文官网地址:https://doi.org/10.1016/j.is.2015.09.005