Published in Volume XXV, Issue 2, 2015, pages 317-355, doi: 10.7561/SACS.2015.2.317

Authors: T. Umarov


This paper addresses the problem of describing and analysing internally consistent data within business process workflow specifications. We use Rodin platform for verifying the correctness of the Event-B models. These models we obtain from an ontology and an associated set of normative constraints by applying mapping rules. The latter enable us to transform these specifications into Event-B modular artefacts. The resulting model, by virtue of the Event-B formalism, is very close to a typical loosely coupled component-based implementation of a business system workflow, but has the additional value of being amenable to theorem proving techniques to check and refine data representation with respect to process evolution. In this paper, we give a formal account of the design specifications defined by Event- B modules and perform verification and validation by using theorem proving techniques provided by Rodin platform.

Full Text (PDF)


[1] A. Jones, M. Sergot. Formal Specification of Security Requirements using the Theory of Normative Positions. In Proceedings of the Second European Symposium on Research in Computer Security, pages 103– 121, 1992. doi:10.1007/BFb0013894.

[2] A. Jones, M. Sergot. On the Characterization of Law and Computer Systems: The Normative Systems Perspective. In Eds. John-Jules Meyer and Roel Wieringa Deontic Logic in Computer Science: Normative System Specification, pages 275–307, Wiley, 1993.

[3] A. Koschmider, A. Oberweis. Ontology Based Business Process Description. In Michele Missikoff and Antonio De Nicola, eds. Proceedings of the Open Interoperability Workshop on Enterprise Modelling and Ontologies for Interoperability, 2005.

[4] C.Y. Kan, X. He. High Level Algebraic Petri nets. Information & Software Technology, 37(1):23–30, 1995. doi:10.1016/0950-5849(94)00438-X.

[5] E. Dijkstra. Guarded commands, nondeterminacy and formal derivation of program. Communications of the ACM, 18(8):453–457, 1975. doi:10.1145/360933.360975.

[6] H.L.R. Finch. Wittgenstein: The Later Philosophy. An Exposition of the Philosophical Investigations. Humanities Press, 1977.

[7] I. Poernomo, T. Umarov. A Mapping from Normative Requirements to Event-B to Facilitate Verified Data-Centric Business Process Management. In Proceedings of 4th IFIP TC 2 Central and East European Conference of Software Engineering Techniques, CEE- SET 2009. Lecture Notes in Computer Science 7054, Advances in Software Engineering Techniques, pages 136 – 149. Springer, 2009. doi:10.1007/978-3-642-28038-2_11.

[8] I. Poernomo, T. Umarov. Implementing a Sound Mapping from Normative Requirements to Event-B Design Blueprints Using MDA. In Proceedings of the 2012 International Conference on Software Engineering Research & Practice. CSREA Press, pages 145–151, 2012.

[9] Information and Knowledge Management in Complex Systems. Proceedings of The 16th Conference on Organisational Semiotics in Organisations K. Liu, K. Nakata, W. Li, D. Galarreta, eds. (2015) ISBN:978-3-319-16273-7 (Print) 978-3-319-16274-4 (Online). doi:10.1007/978-3-319-16274-4.

[10] I. Pörn. The Power of Logic. Blackwell, Oxford, 1970.

[11] I. Pörn. Action Theory and Social Science: Some Formal Models. D. Reidel, Dordrecht, 1977.

[12] J.-R. Abrial, C. M´etayer, L. Voisin. Event-B Language. RODIN Deliverable 3.2, 2005.

[13] J.-R. Abrial. Modeling in Event-B: System and Software Engineering Cambridge University Press, 2010.

[14] J. Searle. Speech Act: An Essay in the Philosophy of Language. Cambridge University Press, 1969.

[15] J. Searle. Expression and Meaning: Studies in the Theory of Speech Acts (essay collection). Duke University Press, 1979.

[16] J. Vautherin. Parallel Systems Specifications with Coloured Petri nets and Algebraic Specifications. In Advances in Petri Nets 1987, the 7th European Workshop on Applications and Theory of Petri nets, pages 293-308, 1987. doi:10.1007/3-540-18086-9_31.

[17] K. Liu. Semiotics in Information Systems Engineering. Cambridge University Press, 2000.

[18] K. Liu, R.J. Clarke, P.B. Andersen, R.K. Stamper. Coordination and communication using signs: Studies in organisational semiotics Kluwer Academic Publishers, 2002.

[19] K. Liu, R.J. Clarke, P.B. Andersen, R.K. Stamper. Organizational semiotics: Evolving a science of information systems Kluwer Academic Publishers, 2002.

[20] L. Lindahl. Position and Change – A Study in Law and Logic. D. Reidel Publishing Company, 1977.

[21] L. Lindahl. Stig Kanger’s Theory of Rights. Logic, Methodology and Philosophy of Science IX, pages 889–911, 1994.

[22] M. Ahtisam, S. Auer, M. Böttcher. From BPEL4WS process model to full OWL-S ontology. In Proceedings of the Third European Semantic Web Conference, 2006.

[23] M. Born, F. Dörr, I. Weber. User-friendly semantic annotation in business process modeling. In Web Information Systems Engineering WISE 2007 Workshops, Lecture Notes in Computer Science, pages 260–271, Springer, 2007. doi:10.1007/978-3-540-77010-7_25.

[24] M. Hepp, D. Roman. An Ontology Framework for Semantic Business Process Management. In Proceedings of the 8th International Conference Wirtschaftsinformatik Universitaetsverlag Karlsruhe, pages 423- 440, 2007.

[25] M. Hepp, F. Leymann, J. Domingue, A. Wahler, D. Fensel. Semantic Business Process Management: A Vision Towards Using Semantic Web Services for Business Process Management. In Proceedings of the IEEE ICEBE 2005, pages 535-540, 2005. doi:10.1109/ICEBE.2005.110.

[26] P. McNamara. Deontic Logic. Stanford Encyclopedia of Philosophy, 2006.

[27] P. Navarro, J. Rodriguez. Deontic Logic and Legal Systems. Cambridge Introductions to Philosophy and Law, 2014

[28] R.-J. Back. Refinement Calculus, Part II: Parallel and Reactive Programs. In Jaco Willem de Bakker, Willem-Paul de Roever, and Grzegorz Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 67–93. Springer-Verlag, 1990. doi:10.1007/3-540-52559-9_61.

[29] R. Kamun, A. Omarov, T. Umarov. Business Requirements: Normative Approach to Behavior Modeling. In Proceedings of the 4th International Symposium on Business Modeling and Software Design, pages 186–195, 2014. doi:10.5220/0005425901860195.

[30] R. Wolfgang. Petri nets: An introduction. Springer, 1985.

[31] S. Halle, R. Villemaire, O. Cherkaoui, B. Ghandour. Model Checking Data-aware Workflow Properties with CTL-FO+. In Proceedings of the 11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007), pages 267–278, 2007. doi:10.1109/EDOC.2007.36.

[32] S. Kanger. Law and Logic. Theoria, 38(3):105–132, 1972. doi:10.1111/j.1755-2567.1972.tb00928.x.

[33] S. Kanger. On Realization of Human Rights. In Action, Logic and Social Theory, 1985.

[34] T. Andrews et al. Business Process Execution Language for Web Services (BPEL4WS). Technical Report, BEA Systems, International Business Machines Corporation, Microsoft, SAP AG, Siebel Systems, 2003.

[35] W.N. Hohfeld. Fundamental Legal Conceptions As Applied in Judicial Reasoning. Dartmouth Publishing, 1964.

[36] W. van der Aalst, K. van Hee. Workflow Management: Models, Methods, and Systems. The MIT Press, 2002.

[37] X. He. PZ Nets: A Formal Method Integrating Petri nets with Z. Information & Software Technology, 43(1):1–18, 2001. doi:10.1016/S0950-5849(00)00134-8.

[38] Y. Gurevich, P. Kutter, M. Odersky, L. Thiele. Abstract State Machines – Theory and Applications. volume 1912 of Lecture Notes in Computer Science, Springer, 2000. doi:10.1007/3-540-44518-8.


  title={Verification and Validation of Formal Data-Centric Business Models},
  author={T. Umarov},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}