1. Home
  2. Issues
  3. Volume 28, Issue 3 (2017)
  4. From Process Models to Concurrent System ...

Informatica


From Process Models to Concurrent Systems in Alvis Language
Volume 28, Issue 3 (2017), pp. 525–545
Pub. online: 1 January 2017      Type: Research Article      Open accessOpen Access
Received
1 July 2016
Accepted
1 March 2017
Published
1 January 2017

Abstract

Business Process Model and Notation (BPMN) is the leading visual notation used for modelling business processes. This paper shows how the Alvis modelling language can be used for formal analysis of BPMN models. Alvis supports graphical modelling of interconnections among subsystems called agents as well as a high-level programming specification for describing the agents’ behaviour. Its advantage is the possibility of formal verification using proven model checking techniques. We propose a translation from the BPMN model to the Alvis representation, which is discussed and evaluated using an illustrative example of a process for evaluation of a student assignment. Thanks to the translation it is possible to perform formal verification of a BPMN model in a high-level concurrent environment. As opposed to some low-level representations, such as Petri nets, semantics of Alvis is close to the original BPMN model. Moreover, if a concurrent system behaviour is specified using a BPMN model, it is possible to generate a formal model (a preliminary implementation) of the system.

References

 
Aguilar, J.C.P., Hasebe, K., Mazzara, M., Kato, K. (2011). Model Checking of BPMN Models for Reconfigurable Workflows. Tech. Rep. CS-TR-1274, Newcastle University.
 
Allweyer, T. (2010). BPMN 2.0. Introduction to the Standard for Business Process Modeling. BoD, Norderstedt.
 
Badica, A., Badica, C. (2011a). Formal verification of business processes represented as role activity diagrams. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (Eds.), Proceedings of the 2011 Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 277–280.
 
Badica, A., Badica, C. (2011b). FSP and FLTL framework for specification and verification of middle-agents. Applied Mathematics and Computer Science, 21(1), 9–25.
 
Baier, C., Katoen, J.P. (2008). Principles of Model Checking. The MIT Press, London.
 
Börger, E. (2012). Approaches to modelling business processes: a critical analysis of BPMN, workflow patterns and YAWL. Software and System Modeling, 11(3), 305–318.
 
Calvanese, D., Dumas, M., Laurson, U., Maggi, F.M., Montali, M., Teinemaa, I. (2016). Semantics and analysis of DMN decision tables. In: Business Process Management: 14th International Conference, BPM 2016, Rio de Janeiro, Brazil, September 18–22, 2016. Proceedings, Vol. 9850, pp. 217–233.
 
Decker, G., Dijkman, R., Dumas, M., García-Bañuelos, L. (2008). Transforming BPMN Diagrams into YAWL nets. In: Dumas, M., Reichert, M., Shan, M.C. (Eds.), Business Process Management, Lecture Notes in Computer Science, Vol. 5240. Business Process Management. Springer, pp. 386–389.
 
Dijkman, R.M., Dumas, M., Ouyang, C. (2007). Formal Semantics and Automated Analysis of BPMN Process Models. Preprint 7115. Tech. rep., Queensland University of Technology, Brisbane, Australia.
 
Dijkman, R., Dumas, M., Ouyang, C. (2008). Semantics and analysis of business process models in BPMN. Information and Software Technology, 50(12), 1281–1294.
 
Emerson, E. (1997a). Model checking and the Mu-calculus. In: DIMACS Series in Discrete Mathematics. American Mathematical Society, pp. 185–214.
 
Emerson, E.A. (1997b). Model checking and the Mu-calculus. In: Immerman, N., Kolaitis, P.G. (Eds.), Descriptive Complexity and Finite Models, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 31. American Mathematical Society, pp. 185–214.
 
Garavel, H., Lang, F., Mateescu, R., Serwe, W. (2007). CADP 2006: a toolbox for the construction and analysis of distributed processes. In: Computer Aided Verification, LNCS, Vol. 4590. Springer-Verlag, pp. 158–163.
 
Jasiul, B., Śliwa, J., Gleba, K., Szpyrka, M. (2014). Identification of malware activities with rules. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (Eds.), Proceedings of the 2014 Federated Conference on Computer Science and Information Systems (FedCSIS), Annals of Computer Science and Information Systems, Vol. 2. IEEE, pp. 101–110.
 
Kluza, K., Maślanka, T., Nalepa, G.J., Ligęza, A. (2011). Proposal of representing BPMN diagrams with XTT2-based business rules. In: Brazier, F.M., Nieuwenhuis, K., Pavlin, G., Warnier, M., Badica, C. (Eds.), 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. Springer-Verlag, pp. 243–248.
 
Kluza, K., Kaczor, K., Nalepa, G.J. (2012). Enriching business processes with rules using the oryx BPMN. In: Rutkowski, L. et al. (Eds.), Artificial Intelligence and Soft Computing: 11th International Conference, ICAISC 2012: Zakopane, Poland, April 29–May 3, 2012, Lecture Notes in Artificial Intelligence, Vol. 7268. Springer, pp. 573–581.
 
Kozen, D. (1983). Results on the propositional μ-calculus. Theoretical Computer Science, 27(3), 333–354.
 
Lam, V.S.W. (2010). Formal analysis of BPMN models: a NuSMV-based approach. International Journal of Software Engineering and Knowledge Engineering, 20(7), 987–1023.
 
Lohmann, N., Verbeek, E., Dijkman, R. (2009). Petri net transformations for business processes – a survey. Transactions on Petri Nets and Other Models of Concurrency, 2, 46–63.
 
Mateescu, R., Sighireanu, M. (2000). Efficient On-the-Fly Model-Checking for Regular Alternation-Free μ-Calculus. Tech. Rep. 3899, INRIA.
 
Matyasik, P., Szpyrka, M., Wypych, M., Biernacki, J. (2016). Communication between agents in Alvis language. In: Proceedings of Mixdes 2016, the 23nd International Conference Mixed Design of Integrated Circuits and Systems, Łódź, Poland, pp. 448–453.
 
Nalepa, G., Bobek, S., Ligęza, A., Kaczor, K. (2011a). HalVA – rule analysis framework for XTT2 rules. In: Bassiliades, N., Governatori, G., Paschke, A. (Eds.), Rule-Based Reasoning, Programming, and Applications, Lecture Notes in Computer Science, Vol. 6826. Springer, Berlin, Heidelberg, pp. 337–344.
 
Nalepa, G.J., Kluza, K., Ernst, S. (2011b). Modeling and analysis of business processes with business rules. In: Beckmann, J. (Ed.), Business Process Modeling: Software Engineering, Analysis and Applications. Business Issues, Competition and Entrepreneurship. Nova Science Publishers, pp. 135–156.
 
Nalepa, G.J., Kluza, K., Kaczor, K. (2013). Proposal of an inference engine architecture for business rules and processes. In: Rutkowski, L. et al. (Eds.), Artificial Intelligence and Soft Computing: 12th International Conference, ICAISC 2013: Zakopane, Poland, June 9–13, 2013, Lecture Notes in Artificial Intelligence, Vol. 7895. Springer, pp. 453–464.
 
Nalepa, G.J., Ligęza, A., Kaczor, K. (2011c). Formalization and modelling of rules using the XTT2 method. International Journal on Artificial Intelligence Tools, 20(6), 1107–1125.
 
OMG (January 2011). Business Process Model and Notation (BPMN): Version 2.0 Specification. Tech. Rep. formal/2011-01-03, Object Management Group.
 
OMG (September 2015). Decision Model and Notation (DMN): Version 1.0. Specification. Tech. Rep. formal/2015-09-01, Object Management Group.
 
O’Sullivan, B., Goerzen, J., Stewart, D. (2008). Real World Haskell. O’Reilly Media, Sebastopol, CA, USA.
 
Ou-Yang, C., Lin, Y.D. (2008). BPMN-based business process model feasibility analysis: a Petri net approach. International Journal of Production Research, 46(14), 3763–3781.
 
Raedts, I., Petković, M., Usenko, Y.S., van derWerf, J.M., Groote, J.F., Somers, L. (2007). Transformation of BPMN models for Behaviour Analysis. In: Augusto, J.C., Barjis, J., Nitsche, U.U. (Eds.), MSVVEIS. INSTICC Press, pp. 126–137.
 
Russell, N., terHofstede, A., van derAalst, W., Mulyar, N. (2006). Workflow Control-Flow Patterns. A Revised View. Tech. Rep. Report BPM-06-22, BPM Center.
 
Silver, B. (2016). DMN Method and Style. Cody-Cassidy Press.
 
Stepaniuk, J., Bazan, J.G., Skowron, A. (2005). Modelling complex patterns by information systems. Fundamenta Informaticae, 67(1–3), 203–217.
 
Szpyrka, M., Matyasik, P., Mrówka, R. (2011a). Alvis – modelling language for concurrent systems. In: Intelligent Decision Systems in Large-Scale Distributed Environments, SCI, Vol. 362. Springer-Verlag, pp. 315–342.
 
Szpyrka, M., Nalepa, G., Ligęza, A., Kluza, K. (2011b). Proposal of formal verification of selected BPMN models with Alvis modelling language. In: Intelligent Distributed Computing V – Proceedings of the 5th International Symposium on Intelligent Distributed Computing, Studies in Computational Intelligence, Vol. 382. Springer, pp. 249–255.
 
Szpyrka, M., Matyasik, P., Wypych, M. (2013). Generation of labelled transition systems for Alvis models using Haskell model representation. In: Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013), CEUR Workshop Proceedings, Warsaw, Poland, Vol. 1032, pp. 409–420.
 
Szpyrka, M., Matyasik, P., Mrówka, R., Kotulski, L. (2014). Formal description of Alvis language with ${\alpha ^{0}}$ system layer. Fundamenta Informaticae, 129(1–2), 161–176.
 
Szpyrka, M., Matyasik, P., Biernacki, J., Biernacka, A., Wypych, M., Kotulski, L. (2016). Hierarchical communication diagrams. Computing and Informatics, 35(1), 55–83.
 
van derAalst, W.M.P., terHofstede, A.H.M. (2005). YAWL: yet another workflow language. Information Systems, 30(4), 245–275.
 
White, S.A., Miers, D. (2008). BPMN Modeling and Reference Guide: Understanding and Using BPMN. Future Strategies Inc., Lighthouse Point, Florida, USA.
 
Wynn, M., Verbeek, H., Aalst, v. d. Hofstede, W., t. Edmond D, A. (2009). Business process verification – finally a reality! Business Process Management Journal, 1(15), 74–92.
 
Ye, J., Sun, S., Wen, L., Song, W. (2008). Transformation of BPMN to YAWL. In: 2008 International Conference on Computer Science and Software Engineering, Vol. 2, pp. 354–359.

Biographies

Szpyrka Marcin
mszpyrka@agh.edu.pl

M. Szpyrka is a full-time professor at AGH University of Science and Technology in Krakow, Poland (Department of Applied Computer Science). He is the author of over 120 publications, from the domains of formal methods, software engineering and knowledge engineering. His fields of interest also include theory of concurrency, systems security and functional programming. He is the leader of the Alvis Project. He is a member of the IEEE Computer Society and the Polish Artificial Intelligence Society (PSSI).

Nalepa Grzegorz J.
gjn@agh.edu.pl

G.J. Nalepa holds a position of professor in AGH UST in Krakow, Poland, Department of Applied Computer Science. Since 1995 he has been actively involved in number of research projects, including Regulus, Mirella, Adder, HeKatE, INDECT, BIMLOQ, Prosecco. He is the author of over 200 papers from the domains of knowledge and software engineering, and intelligent systems. His fields of interest also include computer security and operating systems. He formulated a new design and implementation approach for rule-based systems called XTT (eXtended Tabular Trees). He is involved in many conferences and workshops. In 2011 he published a monograph Semantic Knowledge Engineering. A Rule-Based Approach. He is the President of the Polish Artificial Intelligence Society (PSSI). He is a member of IEEE, and KES International.

Kluza Krzysztof
kluza@agh.edu.pl

K. Kluza holds a position of assistant professor in AGH UST in Krakow, Poland, Department of Applied Computer Science. His main scientific interests focus on software and knowledge engineering, especially business processes and business rules. He obtained MSc in Automatics and Robotics in 2009 at AGH University, Krakow, and MA in Cultural Studies in 2010 at Jagiellonian University, Krakow. In 2015, he obtained PhD in Computer Science at AGH University. He published over 50 papers related to knowledge and software engineering. Krzysztof Kluza is also a Secretary of the Board of the Polish Artificial Intelligence Society.


Full article Cited by PDF XML
Full article Cited by PDF XML

Copyright
© 2017 Vilnius University
Open access article under the CC BY license.

Keywords
business process model verification Alvis modelling language concurrent model formal verification Business Process Model and Notation (BPMN)

Metrics
since January 2020
1170

Article info
views

638

Full article
views

490

PDF
downloads

240

XML
downloads


Share


RSS