CTL Model Repair for Inter-organizational Business Processes Modelled as oWFN

详细信息    查看全文

• 作者：Ulises Martinez-Araiza^&lowast ; ; ^{ulises.martinezaraiza.mx@ieee.org" class="auth_mail" title="E-mail the corresponding author} ; Ernesto Ló ; pez-Mellado^&lowast ; &lowast ; ; ^{elopez@gdl.cinvestav.mx" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Petri nets ; CTL ; Model checking ; Model repair ; Business Process
• 刊名：IFAC-PapersOnLine
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：49
• 期：2
• 页码：6-11
• 全文大小：828 K

文摘

Computation tree logic (CTL) model repair is an approach that extends the model checking technique to obtain new admissible models that can represent the correct design of business processes. Open workflow nets (oWFN) have shown to be adequate to model inter-organizational business processes; this formalism allows performing formal analysis such as model checking. In this work, we adapt a CTL model repair method for bounded and deadlock free Petri nets, to enable it to work with oWFN. The method is illustrated through an example of a placing purchase order process updated by adding a new supplier.