A Formal Verification and Validation of a Collaborative Business Process: Car Assembly Line
摘要
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.