Application of Formal Methods to Verify Business Processes

详细信息    查看全文

• 关键词：Qualitative analysis ; Business Process ; Task model ; Timed automata ; Model checking
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：10090
• 期：1
• 页码：41-58
• 全文大小：2,864 KB
• 参考文献：1.Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal . In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-30080-9_​7 CrossRef
  2.Capel, M., Mendoza, L., Benghazi, K.: Automatic verification of business process integrity. Int. J. Simul. Process Model. 4(3/4), 167–182 (2008)CrossRef
  3.Cheikhrouhou, S., Kallel, S., Guermouche, N., Jmaiel, M.: Enhancing formal specification and verification of temporal constraints in business processes. In: Proceedings of 2014 IEEE International Conference on Services Computing, SCC 2014, pp. 701–708. IEEE Computer Society, Washington (2014). http://​dx.​doi.​org/​10.​1109/​SCC.​2014.​97
  4.Cheikhrouhou, S., Kallel, S., Guermouche, N., Jmaiel, M.: The temporal perspective in business process modeling: a survey and research challenges. Serv. Oriented Comput. Appl. 9(1), 75–85 (2015). http://​dx.​doi.​org/​10.​1007/​s11761-014-0170-x CrossRef
  5.Kossak, F., et al.: How the semantic model can be used. In: A Rigorous Semantics for BPMN 2.0 Process Diagrams, pp. 153–159. Springer International Publishing, Heidelberg (2014). http://​dx.​doi.​org/​10.​1007/​978-3-319-09931-6_​5
  6.Mallek, S., Daclin, N., Chapurlat, V., Vallespir, B.: Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata’. Enterp. Inf. Syst. 9(3), 279–299 (2015). http://​dx.​doi.​org/​10.​1080/​17517575.​2013.​879211 CrossRef
  7.Mendoza, L., Marius, A., Pérez, M., Grimán, A.: Critical success factors for a customer relationship management strategy. Inf. Softw. Technol. 49(8), 913–945 (2007)CrossRef
  8.Morimoto, S.: A survey of formal verification for business process modeling. In: Bubak, M., Albada, G.D., Dongarra, J., Sloot, P.M.A. (eds.) ICCS 2008. LNCS, vol. 5102, pp. 514–522. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-69387-1_​58 CrossRef
  9.OMG: Business Process Model and Notation - v2.0. Object Management Group, Massachusetts (2011). http://​www.​omg.​org/​spec/​BPMN/​2.​0/​PDF
  10.Paternò, F.: Task models in interactive software systems. In: Handbook of Software Engineering and Knowledge Engineering: Recent Advances. World Scientific Publishing Co., Inc., River Edge (2001)
  11.Rüf, J., Kropf, T.: Symbolic model checking for a discrete clocked temporal logic with intervals. In: Proceedings of IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods, pp. 146–163. Chapman & Hall Ltd, London (1997)
  12.Watahiki, K., Ishikawa, F., Hiraishi, K.: Formal verification of business processes with temporal and resource constraints. In: 2011 IEEE International Conference on Systems, Man, and Cybernetics (SMC 2011), pp. 1173–1180. IEEE Computer Society, Los Alamitos (2011)
  
• 作者单位：Luis E. Mendoza Morales (15) (16)
  Carlos Monsalve (15)
  Mónica Villavicencio (15)
  
  15. Facultad de Ingeniería Eléctrica y Computación, FIEC, Escuela Superior Politécnica del Litoral, ESPOL, Campus Gustavo Galindo Km 30.5 Vía Perimetral, P.O. Box 09-01-5863, Guayaquil, Ecuador
  16. Processes and Systems Department, Simón Bolívar University, Valle de Sartenejas, P.O. Box 89000, Caracas, Venezuela
  
• 丛书名：Formal Methods: Foundations and Applications
• ISBN：978-3-319-49815-7
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：10090

文摘

Formal specifications and modeling languages can be used to provide support for Business Process (BP) analysts and designers to verify the behavior of BPs with respect to business performance indicators (i.e., service time, waiting time or queue size). This article presents the application of the Timed Automata (TA) formal language to check BPs modeled with Business Process Model and Notation (BPMN) using the model checking verification technique. Also, a set of transformation rules and two algorithms are introduced to obtain TA-networks from BPMN models, allowing the formal specification of a BP-task model equivalent to the BPMN model. The approach presented here contributes to conduct the qualitative analysis of BPMN models.