A Formal Verification Framework and Associated Tools for Enterprise Modeling: Application to UEML
Abstract:
The aim of this paper is to propose and apply a verification and validation approach to Enterprise Modeling that enables the user to improve the relevance and correctness, the suitability and coherence of a model by using properties specification and formal proof of properties.
Enterprise Modeling versus Enterprise Model Verification: Problematic
A model is a representation of reality that enables a user to understand a system or phenomenon better, to evaluate some of its characteristics, and to share and argue opinions about it with other users.
Usually a model is used to support a decision- making process to determine what actions (design, improve- ment or control) have to be carried out on the system concerned. Enterprise Modeling (EM) [1] is defined by [2] as the art of externalizing enterprise knowledge which adds value to the enterprise or needs to be shared.
It consists of making models of the structure, behavior and organization of the enterprise.
Several approaches, methods, reference models, architecture models, norms and tools have been defined over the last 20 years.
A broad study of these is given in [19] and some of the more important ones are described in Refs. [3,4].
We can cite, for example,
The ICAM Definition (IDef) family which includes several modeling languages (Idef-0 and other) [5],
CIM Open System Architecture (CIMOSA proposing different views of the enterprise: functional, informational, resource and organization) [6],
GRAI and GRAI-GIM (GRAI Integrated Methodology is a methodology for the design and analysis of production systems, and more particularly decision systems, in an enterprise) [7],
Process Specification Language (PSL) [8,9],
TOronto Virtual Enterprise (TOVE) [10],
Business Process Modeling Language (BPML) [11],
Aris [12],
Some reference models, such as:
Purdue Enterprise Reference Architecture (PERA) [13] or
Generalized Enterprise Reference Architecture and
Methodology (GERAM) [14,15] and
some standards [16–18,63,64].
Finally, several tools (ARIS ToolSet, MEGA Process, FirstSTEP, MooGo, Graisoft 1.0, etc.) supporting some of these approaches provide modeling and analysis functionalities enabling the behavior of a part of an enterprise to be represented and investigated.
All of these approaches and tools offer modeling concepts, relations between concepts and constructs that usually highlight the relevant entities that make up an enterprise.
Some of these concepts and relations are common and focus on the same entity as an activity or a process.
However, they are defined differently from one language to another.
For example, a GRAI activity and a PSL activity do not have the same semantic.
On the other hand, some languages propose particular concepts or constructs which do not exist in another languages but are necessary to build models responding to a particular use.
This results a ‘‘Tower of Babel’’ [2] situation in which it is necessary to adopt a consensus and to determine a set of core concepts and constructs for Enterprise Modeling.
The goal is not to define a unique modeling language that will replace all the others.
The goal is to define a pivot modeling language allowing to improve the communication between the existing languages without loss of information and semantics, and to define a set of common concepts which have to be taken into account in the development of future modeling languages.
Researchers have focused on unified languages, such as PSL (dedicated to the representation of manufacturing systems) or Unified Enterprise Modeling Language (UEML) which is dedicated to the representation of business processes [19–22].
Finally, with these modeling languages available, any obtained model can be validated and checked for rigor and robustness [23].
Indeed, it is necessary to guarantee the user a given level of confidence about the suitability, correctness, relevance and fidelity of each model before using it.
In other words, it is necessary to integrate concepts and mechanisms into modeling languages or modeling tools that support or facilitate verification and validation (V&V) tasks:
Verification must confirm [24] by examination and provision of objective evidence that specified requirements have been fulfilled, that is to say to respond to the question ‘‘Is the model well formed?’’
This naturally involves checking the syntax, but also verifying the semantic relevance of the model (the model respects the language construction and behavioral rules and the concepts used are clearly identified and correctly interpreted).
Validation must confirm [24] by examination and provision of objective evidence that the particular requirements for a specific intended use are fulfilled, that is to say ‘‘Is it the intended model?’’ or ‘‘Is the model faithful to reality?’’
This involves assuming that the behavior of the model is equivalent to the behavior of the system, if it exists, or to the requirements, taking into account the modeling hypotheses.
Verification and validation need to provide rigorous arguments in order to convince users of the correct functioning and reliability of a model and of model-based systems before using them [25,26].
It also ensures the coherence between the different models of a given enterprise, thus improving communication and exchange among the different users, or between the different abstraction levels, each one represented by a specific model.
Several techniques and tools make verification and validation possible in different domains [27,28]. Love and Back [29] propose some common ones for Enterprise Modeling, summarized in Table 1.
These go from the most informal ones more suitable for validation to the most formal ones more dedicated to verification. To summarize this table, validation remains difficult without any human experts and verification remains poorly developed.
This article will focus on verification based on formal principles.
Indeed, formal methods [30,31] and tools [28] offer the promise of significant improvements in verification.
They are the only way capable of demonstrating the absence of undesirable model behavior and of making sure that the model will function as required.
On the other hand, it is widely recognized that these methods are expensive, not easy to use and therefore not very accessible.
The reason is that formal approaches cannot be understood and handled by most experts in the domain, and especially because they are not yet used in the EM field.
As a matter of fact, their use is not always very interesting for a non-specialist because it lays down too strict and a limited vision of the modeled system and leads to uncertain delays before obtaining the needed results.
This paper presents the concepts and tools supporting an Enterprise Modeling Verification methodology based on formal proof of properties, taking into account the following main concepts and mechanisms:
A modeling language enabling a property to be described and handled [32].
An ontology allowing us to develop a common vocabulary [33] composed of sets of related concepts and relations dedicated to Enterprise Model Verification. This ontology allows us to propose extensions to UEML.
A Properties Reference Repository (PRR) [34] is a predefined properties database in which the user can choose, select and specify different properties which classically have to be proved on a model. We describe an EM PRR below.
A set of formal verification mechanisms [35,36] based on Conceptual Graphs [37].
In order to demonstrate this work, the proposed approach will be applied to UEMLVersion 1.0 [20], whose meta model is presented in Fig. 1.
UEML should be able to translate a business process model into another modeling language without any distortion of semantics. So, it will be considered here as a modeling language even though that is not its prime objective.
All the proposed concepts, relations and mechanisms can be added as proposed to UEML 1.0 enabling verification tasks to be performed during the modeling process.
Conclusion:
This paper proposes a methodology for achieving the verification, and to some extent the validation (V&V) for Enterprise Modeling.
This methodology has been applied here to a common and relevant modeling language named UEML and is supported by a set of interconnected tools:
The Unified Property Specification Language [50] framework to provide the property specification and handling mechanisms.
Rational Rose for building parts of the Ontology and generating interchange files (XML, CogXML and SQL) so as to establish communication without loss of meaning between all the other tools.
Generic Modeling Environment (GME) [49] used for UEML processing and model translation.
Cogitant 5.1.4 [57] to provide verification mechanisms.