Abstract
Business Process Modeling Notation (BPMN) is one of the standard business process (BP) description, which is established by the Object Management Group (OMG). In addition to the notational elements to control the task execution sequence, BPMN provides us with those elements to express the time constraints such as deadline and delay. Since the behavior of BP models with the time constraints become complicated, it seems difficult to verify them using BPMN alone. This paper presents a method to make the rigorous verification possible for the models expressed in the form of BPMN, by converting them into the simulatable timed CPN models.