Paper Info
Title
Enabling model checking for collaborative process analysis: from BPMN to ‘Network of Timed Automata’
Abstract
Interoperability is a prerequisite for partners involved in performing collaboration. As a consequence, the lack of interoperability is now considered a major obstacle. The research work presented in this paper aims to develop an approach that allows specifying and verifying a set of interoperability requirements to be satisfied by each partner in the collaborative process prior to process implementation. To enable the verification of these interoperability requirements, it is necessary first and foremost to generate a model of the targeted collaborative process; for this research effort, the standardised language BPMN 2.0 is used. Afterwards, a verification technique must be introduced, and model checking is the preferred option herein. This paper focuses on application of the model checker UPPAAL in order to verify interoperability requirements for the given collaborative process model. At first, this step entails translating the collaborative process model from BPMN into a UPPAAL modelling language called 'Network of Timed Automata'. Second, it becomes necessary to formalise interoperability requirements into properties with the dedicated UPPAAL language, i.e. the temporal logic TCTL.
Year
DOI
Venue
2015
10.1080/17517575.2013.879211
Enterprise IS
Keywords
Field
DocType
verification,model transformation,model checker,network of timed automata,interoperability requirements,collaborative process
Obstacle,Model transformation,Model checking,Systems engineering,Computer science,Interoperability,Automaton,Process analysis,Semantic interoperability,Business Process Model and Notation
Journal
Volume
Issue
ISSN
9
3
1751-7575
Citations 
PageRank 
References 
5
0.51
4
Authors
4
Name
Order
Citations
PageRank
Sihem Mallek1162.01
Nicolas Daclin210211.54
Vincent Chapurlat37113.14
Bruno Vallespir411520.01