Abstract: Business 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.