Search

This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories., In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636

International audience; While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation.Up to now, Isabelle’s document preparation system lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.In this paper, we present Isabelle/DOF, a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for conventional typesetting as well as formal development. We show how to model document ontologies inside Isabelle/DOF, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support.

Requirements engineering plays a crucial role in the development process of an information system as it aims at providing a complete and accurate requirement specification. In the life cycle of a Data Repository (\({\mathcal {D}}{\mathcal {R}}\)) such as a database or a data warehouse, the requirements are mainly used to define the conceptual model once they have been identified from the informal specification. In this paper, we study the interest of requirements in the other phases of the \({\mathcal {D}}{\mathcal {R}}\) life cycle. As the data integration problem, handled in the Extract, Transform, Load (ETL) phase, comes from the heterogeneity of requirements, we introduce a requirement integration framework based on ontologies and a generic model to unify the used vocabularies and requirement languages. Then we propose an approach to check the consistency of the requirements, w.r.t. the integrity constraints defined on the logical schema using the formal B method. We also show that requirements help define appropriate access structures such as indexes and materialized views to optimize SQL queries of a \({\mathcal {D}}{\mathcal {R}}\). Our approach is based on transformation rules that identify important queries that will be executed on a \({\mathcal {D}}{\mathcal {R}}\) directly from the requirements. The experiments conducted on the Star Schema Benchmark (SSB) confirm the interest of this approach for the selection of different optimization structures. Finally, we present the OntoReqTool that implements the previous functionality on top of the OntoDB/OntoQL platform.

Multimodal human---computer interaction (HCI) combine modalities at an abstract specification level in order to get information from the user (input multimodality) and to return information to the user (output multimodality). These multimodal interfaces use two mechanisms: first, the fusion of information transmitted by the user on different modalities during input interaction and second, the fission or decomposition of information produced by the functional core in order to distribute the composite information on the different modalities during output interaction. In this paper, we present a generic approach to design output multimodal interfaces. This approach is based on a formal model, composed of two models: semantic fission model for information decomposition process and allocation model for modalities and media allocation to composite information. An Event-B formalization has been proposed for the fission model and for allocation model. This Event-B formalization extends the generic model and support the verification of some relevant properties such as safety or liveness. An example of collision freeness property verification is presented in this paper.

International audience; When designing a hardware or a software system, the inte-gration of domain constraints becomes a determining factor to ensurea great match with the system requirements. This domain knowledge ismost often modelled using ontologies that allow to express the domaindata properties. In this paper, we propose an approach to integrate do-main ontologies into a system development process based on Event-B. Itconsists to annotate Event-B models using the ontology concepts, thisassumes a formalization of the domain ontology in the Event-B method.Therefore, we propose an extensible generic transformation approachwhich develops an Event-B specification based on an ontology describedin an ontological language. The integration of the Event-B descriptionof a domain ontology allows to constrain the system under design withthe domain ontology and to validate domain properties.

Several languages for describing Web service compositions, like BPEL (Business Process Execution Language), make use of fault and compensation constructs to handle internal and/or external runtime errors of the composed service. This situation particularly occurs for transactional services. However, the absence of a rigorous definition of these BPEL constructors makes it difficult to correctly define the transactional behaviour of a BPEL process. The definitions of such constructs are usually given by their informal descriptions available in the standards. Our contribution proposes an approach to formally define the semantics of these operators. Thus, this paper presents a new Event-B semantics for formal modelling of Web service compositions that covers the scope, the fault and the compensation handlers introduced by the BPEL language specification. It also proposes a methodology showing how we can use Event-B method to design transactional BPEL processes. The proposed approach is illustrated by a case study.

International audience; The Web service composition can be defined as the process of combining existing services to produce new ones. Indeed, composition to develop higher-level services, so-called composite services, by re-using existing services is Service Oriented Architectures (SOA) core capability. For this purpose, languages such as BPEL and platforms like the orchestration engine appeared for the specification and the implementation of service compositions. However, the expressiveness of these languages deals only with functional compositions and does not take into account the composite Web services properties validation and the tools associated to these languages do not support simulation of behavioural requirements.Our contribution consists in using software agents to provide a simulation tool to BPEL, to observe agents behaviours and to evaluate properties. Simulation plays an important role by exploring ”what-if” questions during the process composition phase. The proposed approach is implemented using JADE platform.

Requirements engineering aims at providing a requirement specification with some nice properties such as completeness or accuracy. In the lifecycle of a Data Repository (\(\mathcal{D}\mathcal{R}\)), user requirements are usually assumed to be homogenous and used mainly to define the conceptual model of a \(\mathcal{D}\mathcal{R}\). In this paper, we study the interest of the requirements in the other phases of the life cycle of a \(\mathcal{D}\mathcal{R}\). We propose a generic model based on ontologies to unify the used vocabularies and requirements languages. Then we extend this model using the formal method B to check the consistency of the requirements w.r.t. the integrity constraints defined on the logical schema. Finally we propose to select optimization structures of a \(\mathcal{D}\mathcal{R}\) using the user requirements instead of SQL queries. Several experiments on the Star Schema Benchmark (SSB) confirm the interest of our proposition.

International audience; With the development of the web, a huge number of services available on the web have been published. These web services operate in several application domains like concurrent engineering, semantic web, system engineering or electronic commerce. Moreover, due to the ease of use of the web, the idea of composing these web services to build composite ones defining complex workflows arose. Even if several industrial standards providing specification and/or design XML-oriented languages for web services compositions description, like BPEL, CDL, OWL-S, BPMN, the activity of composing web services remains a syntactically based approach. Due to the lack of formal semantics of these languages, ambiguous interpretations remain possible and the validation of the compositions is left to the testing and deployment phases. From the business point of view, customers do not trust these services nor rely on them. As a consequence, building correct, safe and trustable web services compositions becomes a major challenge. It is well accepted that the use of formal methods for the development of infor-mation systems has increased the quality of such systems. Nowadays, such methods are set up not only for critical systems, but also for the development of various infor-mation systems. Their formal semantics and their associated proof system allow the system developer to establish relevant properties of the described information sys-tems. This talk addresses the formal development of models for services and their com-position using a refinement and proof based method, namely the Event B method. The particular case of web services and their composition is illustrated. We will focus on the benefits of the refinement operation and show how such formalization makes it possible to formalise and prove relevant properties related to composition and adaptation. Moreover, we will also show how implicit semantics carried out by the services can be handled by ontologies and their formalisation in such formal develop-ments. Indeed, once ontologies are formalised as additional domain theories beside the developed formal models, it becomes possible to formalise and prove other prop-erties related to semantic domain heterogeneity.

International audience; The Service-Oriented Architectures (SOA) are increasingly used in various application domains. Nowadays various Services operate on the Web and access various critical resources such as databases. These services are called transactional web services when they perform transactional actions. This kind of Services must verify the relevant constraints related to transactional systems. In our work, we focus on web services described with BPEL [1]. In the BPEL language, a composite Web Service is implemented by a process that consists of activities such as the messaging activities invoke and reply, used for interacting with other web services and the structured activities sequence, flow and scope, acting as containers for their nested activities. BPEL provides some support for transactions through its fault and compensation handlers undoing the effects of completed activities. In most related work [2,3], validation of the web services composition and workflow shows how to model transactional behaviors and involves the verification of behavioral properties. In our work, we sketch a methodology showing how Event B models [4,5] obtained by the approach described in [6] can be used to prove web services transactional properties. Transactional services that access and manage critical resources are isolated in a scope element with compensation and fault handlers. When modelling fault and compensation handlers by a set of events, it becomes possible to model and check the properties related to transactional web services. These properties are encoded in the INVARIANTS clause in order to guarantee consistency of the manipulated resources.

International audience; Several web services compositions languages and standards are used to describe different applications available over the web. These languages are essentially syntactic ones, their descriptions remain informal and are based on graphical notations. They do not offer any guarantee that the described services achieve the goals they have been designed for. The objective of this paper is twofold. First, it focusses on the formal description, modelling and validation of web services compositions using the Event B method. Second, it suggest a refinement based method that encodes the BPEL models decompositions. Finally, we show that relevant properties formalized as Event B properties can be proved. A tool encoding this approach is also available.

The Web Services composition defines a processthat involves various independent Web Services to performa complex function. This process is described with a standardlanguage (BPEL) and executed by tools supporting thislanguage. This kind of languages describes the behavior ofdifferent distributed services together, but it does not supportthe verification nor the validation of behavioral requirements.In our work, we are interested in the formal validation ofWeb Services composition. Formal models are extracted fromBPEL specifications and checked. Most previous work is basedon Web Services composition formalizations using Petri nets,process algebra or transition systems. The model checkingtechnique is set-up to validate such descriptions.In this paper, we present a proof and refinement basedapproach for the formal representation, verification and validation of Web Services compositions using the Event B method.

International audience; Cet article s'intéresse à la validation et à la vérification formelles d'IHM Multi-Modales (IHM3). Il décrit une partie des résultats obtenus dans le cadre du projet RNRT VERBATIM, dont l'objet est la VERification Biformelle et l'Automatisation du Test des Interfaces Multimodales. Ce projet s'intéresse, entre autres, à la mise en œuvre d'une technique formelle fondée sur la preuve : la méthode B événementiel. Nous discutons les apports de cette technique pour la conception d'IHM3, en particulier, sa capacité à exprimer et à vérifier des propriétés de la famille CARE. Notre approche utilise et propose de formaliser des notations et techniques semi-formelles issues du domaine des IHM.