Proposal of Formal Verification of Selected BPMN Models with Alvis Modeling Language

Authors: Marcin Szpyrka, Grzegorz J. Nalepa, Antoni Ligęza, Krzysztof Kluza

Abstract: BPMN is a leading visual notation for modeling business processes. Although there is many tools that allows for modeling using BPMN, they mostly do not support formal verification of models. The Alvis language was developed for modeling and verification of embedded systems. However, it is suitable for the modeling of any information systems with parallel subsystems. The goal of this paper is to describe the concept of using Alvis for a formal verification of selected BPMN models. In the paper a translation from BPMN to Alvis model is proposed. The translation is discussed and evaluated using a simple yet illustrative example.

Keywords: BPMN, Alvis, formal verification

Paper: http://www.springerlink.com/content/m181144037q67271/

Cite as:

Szpyrka, M., Nalepa, G.J., Ligeza, A., Kluza, K: Proposal of Formal Verification of Selected BPMN Models with Alvis Modeling Language. In Brazier, F. M. T., et al.: Intelligent Distributed Computing V: Proceedings of the 5th International Symposium on Intelligent Distributed Computing – IDC 2011, Delft, The Netherlands – October 2011. Studies in Computational Intelligence vol. 382. Berlin, Heildelberg, Springer-Verlag, pp. 249–255 (2011)

Bibtex:

@InCollection{szpyrka2011idc,
  author = 	 {Marcin Szpyrka and Grzegorz J. Nalepa and Antoni Lig\k{e}za and Krzysztof Kluza},
  title = 	 {Proposal of Formal Verification of Selected {BPMN} Models with {Alvis} Modeling Language},
  booktitle = 	 {Intelligent Distributed Computing V. Proceedings of the 5th International Symposium on Intelligent Distributed Computing -- IDC 2011, Delft, the Netherlands -- October 2011},
  pages = 	 {249--255},
  publisher =	 {Springer-Verlag},
  year =	 {2011},
  editor =	 {Frances M.T. Brazier and Kees Nieuwenhuis and Gregor Pavlin and Martijn Warnier and Costin Badica},
  volume = 	 {382},
  series =	 {Studies in Computational Intelligence}
}

Cited by:

If you cite this publication, let me know about it, and it will be listed here.