Formal semantics for refinement verification of entreprise models

In this dissertation we investigate how Business/IT alignment in enterprise models can be enhanced by using a software engineering stepwise refinement paradigm. To have an IT system that supports an enterprise and meets the enterprise business needs, management seeks to align business system with IT systems. Enterprise Architecture (EA) is the discipline that addresses the design of aligned business and IT systems. SEAM is an Enterprise Architecture method, developed in the Laboratory of Systemic Modeling (LAMS) at EPFL. SEAM defines a visual language for building an enterprise model of an organization. In this work, we develop a theory and propose a technique to validate an alignment between the system specifications expressed in the SEAM language. We base our reasoning on the idea that each system (an organization, a business system, or an IT system) can be modeled using a set of hierarchical specifications, explicitly related to each other. Considering these relations as refinement relations, we transform the problem of alignment validation into the problem of refinement verification for system specifications: we consider that two system specifications are aligned if one is correctly refines the other. Model-driven engineering (MDE) defines refinement as a transformation between two visual (or program) specifications, where a specification is gradually refined into an implementation. MDE, however, does not formalize refinement verification. Software engineering (SE) formalizes refinement for program specifications. It provides a theory and techniques for refinement verification. To benefit from the formal theories and the refinement verification techniques defined in SE, we extend the SEAM language with additional concepts (e.g. preconditions, postconditions, invariants, etc). This extension enables us to increase the precision of the SEAM visual specifications. Then we define a formal semantics for the extended SEAM modeling language. This semantics is based on first-order logic and set theory; it allows us to reduce the problem of refinement verification to the validation of a first-order logic formula. In software engineering, the tools for the automated analysis of program specifications are defined. To use these tools for refinement verification, we define a translation from SEAM visual specifications to formal specification languages. We apply, using case studies, our theory and technique in several problem areas to verify: (1) if a business process design and re-design correspond to high level business process specifications; (2) if a service implementation corresponds to its specifications. These case studies have been presented to a group of domain experts who practice business/IT alignment. This inquiry has shown that our research has a potential practical value.