Verification and Validation of Formal Data-Centric Business Models

Scientific Annals of Computer Science

article

T. Umarov¹ 

[1] Department of Management Information Systems, Faculty of Information Technology, Kazakh-British Technical University

关键词: Event-B;    verification;    validation;    business process;    formal specifications;    Rodin platform.;   

DOI  :  10.7561/SACS.2015.2.317

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

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 EventB modules and perform verification and validation by using theorem proving techniques provided by Rodin platform.

【 授权许可】

CC BY-ND