The current work is based on Business Processes (BP) formal verification and validation. The purpose is the design, the specification, and the implementation of a simulation application for assembly-line cars. The case study has been chosen because it provides different views for several business processes: the view of the administrator that allows system configuration, account management, and component setting. The view of the technical staff is to publish the current tacked measurements, edit reports to understand the situation of the current system, locate the damage, and perform onsite maintenance. The analysis phase identifies the system business processes components (robotic arms and supply chain). The design phase uses UML diagrams. The specification phase adopts the UPPAL software tool to elaborate a timed automata in order to formally verify the system behavior by CTL, system synchronization, business process simulation, and validation of the most properties. The implementation phase uses the most appropriate software tools for developing the simulation system.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Formal Verification and Validation of a Collaborative Business Process: Car Assembly Line

  • Hanane Ouaar

摘要

The current work is based on Business Processes (BP) formal verification and validation. The purpose is the design, the specification, and the implementation of a simulation application for assembly-line cars. The case study has been chosen because it provides different views for several business processes: the view of the administrator that allows system configuration, account management, and component setting. The view of the technical staff is to publish the current tacked measurements, edit reports to understand the situation of the current system, locate the damage, and perform onsite maintenance. The analysis phase identifies the system business processes components (robotic arms and supply chain). The design phase uses UML diagrams. The specification phase adopts the UPPAL software tool to elaborate a timed automata in order to formally verify the system behavior by CTL, system synchronization, business process simulation, and validation of the most properties. The implementation phase uses the most appropriate software tools for developing the simulation system.