Journal of Software Engineering1819-43112152-0941Asian Network for Scientific Information10.3923/jse.2014.58.74YuRuiqiang HuangZhiqiu WangLin ZhangHongjie 2201482Business Process Modeling Notation (BPMN) is the most influential graphical
modeling notation in service composition aspect and has been widely used in
modeling the Web service composition system, however BPMN lacks of formal semantics
and can not be verified formally and automatically. Extended object Petri net
(EOPN for short) is presented in order to model and verify BPMN process formally.
Guard, flow valve and time constraint are introduced into EOPN. Because state
class method for analyzing time Petri net is destitute of global temporal constraints,
timestamp state class method is developed and the corresponding analysis approach
is also presented. The enabled conditions of transition are listed and the firing
condition and rules of transition of EOPN are discussed in detail. Mapping rules
from BPMN to EOPN are depicted in detail. An example is provided for illustrating
the feasibility of mapping BPMN process diagram to EOPN model and verifying
its rightness formally.]]>Berthomieu, B. and M. Menasche,19831983pp: 4146Berthomieu, B. and M. Diaz,199117259273Berthomieu, B. and F. Vernadat,20032003pp: 442-457pp: 442-457Dijkman, R.M., M. Dumas and C. Ouyang,20085012811294Hinz, S., K. Schmidt and C. Stahl,20052005pp: 220-235pp: 220-235Lakos, C.,20012001pp: 1-37pp: 1-37Merlin, P.,19741974OMG,20062006OMG,20082008Ramchandani, C.,1974Valk, R. and C. Girault,2003Van der Aalst, W.M.P. and A.H.M. Ter Hofstede,2000254369Valk, R.,19981998pp: 1-24pp: 1-24Valk, R.,20042004pp: 819-848pp: 819-848Zhehui, W.,2006Yi, Y.C.,2005Jian, Y. and H. Yanbo,2006Yu, R., Z. Huang and L. Wang,20092009pp: 243246Kohler, M. and H. Rolke,20042004pp: 278-297pp: 278-297