Search

International audience; Ontologies are structured data models used to describe a set of concepts related to a specific domain, they describe also the semantic properties of these concepts. Formal development process aims to develop a system with respect to properties or constraints. The IMPEX project is interested in involving domain constraints as soon as possible into formal development process, it proposes to integrate the ontologies descriptions in an Event-B development process. This approach assumes to develop a transformation step of the ontologies constructs from their initial description in an ontological language (OWL, OntoML ...) to Event-B. A first version of this transformation approach for OWL ontologies based on a generic and extensible architecture has been developed, it is supported by the OntoEventB tool. An evolution of this approach to include OntoML ontologies and new features is presented in this paper.

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.

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.

International audience; System engineering is a complex discipline[1], which is becoming more and more complicated by the heterogeneity of the subsystem components[2] and of the models involved in their design. This complexity can be managed only through the use of formal methods[3]. However, in general the engineering of software in such systems leads to a need for a mix of modelling languages and semantics; and this often leads to unexpected and undesirable interactions between components at all levels of abstraction[4]. There are currently no generally applicable tools for dealing with this heterogeneity of interactions in the engineering of complex systems.

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.

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.

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.

International audience; This paper focuses on the formal validation and verification of multi-modal human computer interfaces. It describes part of the obtained results of the French RNRT VERBATIM project whose purpose is the Multimodal Interfaces BIformal Verification and Test Automation. This project focuses on the application of a formal technique, namely the event B method. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. We outline the capability of this technique to support the design of multi-modal human computer interfaces, in particular, the capability to support the expression and the verification of properties issued from the CARE family. The proposed approach uses notations and semi-formal techniques issued from the HCI design area. We apply our approach on a case study called "CLIPS Yellow Pages".