The Community for Technology Leaders
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (2017)
Urbana, IL, USA
Oct. 30, 2017 to Nov. 3, 2017
ISBN: 978-1-5386-3976-4
pp: 217-228
Flavio Corradini , School of Science and Technology, University of Camerino, Camerino, Italy
Fabrizio Fornari , School of Science and Technology, University of Camerino, Camerino, Italy
Andrea Polini , School of Science and Technology, University of Camerino, Camerino, Italy
Barbara Re , School of Science and Technology, University of Camerino, Camerino, Italy
Francesco Tiezzi , School of Science and Technology, University of Camerino, Camerino, Italy
Andrea Vandin , DTU Compute, Technical University of Denmark, Lyngby, Denmark
ABSTRACT
Business Process Modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe activities of complex organisations. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nevertheless, the lack of formal semantics hinders the automatic verification of relevant properties. This paper presents a novel verification framework for BPMN 2.0, called BProVe. It is based on an operational semantics, implemented using MAUDE, devised to make the verification general and effective. A complete tool chain, based on the Eclipse modelling environment, allows for rigorous modelling and analysis of Business Processes. The approach has been validated using more than one thousand models available on a publicly accessible repository. Besides showing the performance of BProVe, this validation demonstrates its practical benefits in identifying correctness issues in real models.
INDEX TERMS
Semantics, Analytical models, Logic gates, Business, Software systems, Tools, Collaboration
CITATION

F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi and A. Vandin, "BProVe: A formal verification framework for business process models," 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 217-228.
doi:10.1109/ASE.2017.8115635
395 ms
(Ver 3.3 (11022016))