首页 | 本学科首页   官方微博 | 高级检索  
     


Property specification,process verification,and reporting – A case study with vehicle-commissioning processes
Affiliation:1. Department of Mechanical and Industrial Engineering, Toronto University, 5 King’s College Road, Toronto, Ontario, M5S 3G8, Canada;2. Department of Industrial Engineering, Ajou University, San 5, Woncheon-dong, Yeongtong-gu, Suwon, Korea
Abstract: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.
Keywords:Property specification  Business process management  Workflow management  Verification  Model checking  Petri net  Industrial processes  Vehicle commissioning processes
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号