Search

International audience

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.

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; 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.

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

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; 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.

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

International audience

Multi-modal Human-Computer Interfaces (HCI) allowinterface designers to combine interactive modalities inorder to increase interactive systems robustness and us-ability. In particular, output multi-modal interfaces al-low the system to return the information to the userby using several modalities and media. In order to de-sign such interfaces for critical systems, we proposeda generic formal model for the design of output multi-modal interfaces. The proposed model formally speci-fies an output multi-modal interface and enables prop-erties verification. It consists of two successive mod-els: the fission model that describes the semantic de-composition of information produced by the functionalcore into elementary information, and the allocationmodel that specifies the allocation of modality/mediapairs for each elementary information. In a previouswork (Mohand-Oussaid, Ait-Sadoune, and Ait-Ameur2011), we have proposed an Event-B implementation ofthe fission model. In this paper, we present an Event-Bformalization of the allocation model.

International audience; With the aim to provide a complete tool for the web services compositions validation, we have integrated various plugins in a single platform. This platform is based on the Eclipse core and contains the WSDL and BPEL editors plugins~(1), the BPEL2B (2) and B2EXPRESS (3) developed plugins and the various plugins of the RODIN platform (4). Different views are offered by this platform : WSDL and BPEL editors to describe different web services and their orchestration graphically or using the XML syntax, BPEL2B plugin to transform the WSDL/BPEL specifications onto Event-B models, the different plugins of RODIN to perform web services composition validation on the obtained Event-B model and the B2EXPRESS plugin to animate the obtained Event-B model.

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.

Output multi-modal human-machine interfaces combine semantically output medias and modalities to increase interaction machine capabilities. In order to provide a rigorous development approach for these interfaces, we have proposed a generic formal model that formally describes the output multimodal interface construction starting from the information generated by the functional core. This formal model is composed of two sub-models: the first one dedicated to the semantic fission of information and the second one relative to the allocation of modalities and medias for information. This paper presents an Event-B implementation of the semantic fission submodel.

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; Le processus de composition de services Web est défini par une chorégraphie ou une orchestration de ces services. Les langages de description de la chorégraphie ou d'orchestration sont généralement décrits d'une manière informelle dans les spécifications et les outils associés n'offrent pas la possibilité de vérifier et de valider formellement le comportement et les propriétés du service composé obtenu. Dans cet article, on s'intéresse à la vérification formelle de l'orchestration de services décrite avec le langage BPEL en utilisant la méthode B Événementiel. L'approche proposée se base sur le raffinement pour la structuration du développement d'un processus BPEL, et sur la preuve de théorèmes pour l'établissement de propriétés. Cet article présente également l'outil BPEL2B qui implémente l'approche proposée.

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.

Web services compositions are defined using languages supporting the descrip- tions of orchestration and choreography. BPEL is the most well known and used orchestration language. It describes the behavior of the process that specifies the composition of web ser- vices but it does not support verification and validation of behavioral requirements. In our work, we are interested in the formal validation of web services orchestrations. We propose a proof and refinement based approach for the formal representation, verification and validation of web services compositions using the Event B method. This paper presents the BPEL2B translator that automates the translation of BPEL into Event B models.

International audience; Les architectures d'un système interactif reposent sur la séparation du noyau fonctionnel et de l'interface utilisateur du logiciel. Le développement de ces deux modules implique l'utilisation de techniques et d'approches différentes et engendre un développement hétérogène. La validation du système interactif, peut être une étape complexe puisque ces modules sont développés séparément. Dans le cadre du projet RNRT Verbatim, l'étude de différents scénarios de développement formels des systèmes interactifs multimodaux, a été menée en utilisant la méthode B événementiel. Le raffinement est mis en œuvre pour structurer les développements et la preuve pour établir les propriétés. Cet article s'intéresse principalement à la liaison entre les deux modules d'un système interactif que sont le noyau fonctionnel et l'interface utilisateur. Quatre scénarios de développement différents sont étudiés et comparés.

International audience; L'outil B2EXPRESS est un animateur de modèles B événementiel fondé sur l'instanciation de modèles de données exprimés dans le langage EXPRESS. Chaque construction de modèle B (substitutions, invariant, ensembles, variables, etc) est transformée en une construction de modèle EXPRESS (entité, attribut, regèles locales et globales). L'animation consiste à définir des instances des différentes entités du modèle EXPRESS obtenu et de contrôler les contraintes associées.

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; Les architectures d'un système interactif reposent sur la séparation du noyau fonctionnel de l'interface utilisateur du logiciel. Le développement de ces deux modules implique l'utilisation de techniques et d'approches différentes. La validation du système interactif peut être une étape complexe puisque ces modules sont développés séparément. Dans le cadre du projet RNRT Verbatim*, l'étude de différents scénarios de développement formels des systèmes interactifs multi-modaux, a été menée en utilisant la méthode B dans sa version "B événementiel". Cet article présente une partie des résultats de cette étude. Le raffinement est mis en œuvre pour structurer les développements et la preuve pour établir les propriétés. Il s'intéresse principalement à la liaison (lors de leur composition) entre les deux modules d'un système interactif que sont le noyau fonctionnel et l'interface utilisateur. Quatre scénarios de développement différents, représentant formellement cette liaison, sont étudiés et comparés. Cette comparaison est réalisée sur la base du nombre d'obligations de preuve générées et relatives aux propriétés décrites dans les spécifications. Une étude de cas décrivant un système interactif multi-modal, illustrant ces scénarios et leur comparaison est utilisée tout au long de cet article.

La naissance de nouveaux dispositifs d'interaction (écran tactiles, gants à retour d'effort, etc.), l'utilisation des machines dans différentes situations avec des utilisateurs différents, l'utilisation de modes différents (visuel, auditif, etc.) ont engendré une complexité dans l'usage des machines. L'intégration de ces différents médias a donné lieu à un nouveau type d'interfaces homme-machine dites : interfaces homme machine multimodales (IHM3). L'usage des IHM multimodales permet à l'utilisateur de communiquer de manière intuitive avec la machine, cependant, l'utilisation de manière séquentielle voire simultanée de plusieurs modalités d'interaction (parole, geste, etc.) rend la représentation des informations échangées plus ardue et implique un processus de développement et de validation plus complexe. L'introduction des systèmes interactifs informatisés dans les systèmes de transport, généralement critiques, exige un haut niveau de fiabilité pour ces derniers et impose des approches de conception sûres garantissant le respect des spécifications. Ces approches habituellement consacrées au développement du noyau fonctionnel des systèmes se tournent à présent vers le développement des interfaces, partie intégrante du système qui de surcroît joue un rôle déterminant dans ce type de systèmes tant la communication est importante. Ceci, a donné naissance à des travaux qui s'intéressent à la modélisation et la vérification formelles des systèmes interactifs multimodaux. Dans ce chapitre, nous nous proposons d'aborder la conception formelle des IHMs multimodales. Dans la première partie nous présentons les principaux concepts liés à la multimodalité. Dans la deuxième partie, nous exposons succintement les principes des approches de conception et de vérification formelles. Les troisième et quatrième parties sont consacrées respectivement à la multimodalité en entrée et en sortie, nous y présentons les principaux travaux de modélisation de la multimodalité, ainsi que les modèles formels en entrée et en sortie proposés. Pour chaque modèle formel, nous définissons la syntaxe et la sémantique, enfin, nous illustrons le modèle à travers une interface homme-machine multimodale se rapportant au domaine des transports.

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".

International audience; The Web Services composition defines a process that involves various independent Web Services to perform a complex function. This process is described with a standard language (BPEL) and executed by tools supporting this language. This kind of languages describes the behavior of different distributed services together, but it does not support the verification nor the validation of behavioral requirements. In our work, we are interested in the formal validation of Web Services composition. Formal models are extracted from BPEL specifications and checked. Most previous work is based on Web Services composition formalizations using Petri nets, process algebra or transition systems. The model checking technique is set-up to validate such descriptions. In this paper, we present a proof and refinement based approach for the formal representation, verification and validation of Web Services compositions using the Event B method.

The ability to compose existing services to provide more complex functionality is one of the main benefits of SOA architecture. This services compositions process, especially Web services, is generally defined by a choreography or an orchestration of atomic services. These compositions are seen as a states-transitions systems expressing the communication protocol between the participating services. Services Workflows description languages, expressing these compositions, suffer from the lack of formal semantics and the presence of ambiguities in their constructors definitions in standards defining these languages. The associated tools do not offer the possibility to formally verify and validate the behaviour and the obtained services compositions properties. This thesis focuses on modelling and formal verification of the Web services composition described with the BPEL standard using the B event method. The proposed approach models the static and dynamic parts of BPEL and is based on refinement for structuring the BPEL process development. The theorem proving technique is used for setting properties. One-to-one link is guaranteed between the BPEL elements and their B Event corresponding. This correspondence provides assistance to developers to improve the quality of the BPEL process. This approach has been implemented in the BPEL2B tool.; La possibilité de composer des services préexistants pour offrir des fonctionnalités plus complexes est l’un des apports principaux des architectures SOA. Ce processus de composi- tion de services, en particulier les services Web, est généralement défini par une chorégraphie ou une orchestration de services atomiques. Ces compositions sont vues comme un système états-transitions exprimant le protocole de communication entre les services participants. Les langages de description de Workflows de services, exprimant ces compositions, souffrent de l’absence de sémantique formelle et de la présence d’ambigüités dans la définition de leurs constructeurs au sein des standards définissant ces langages. Les outils associés à ces langages n’offrent pas la possibilité de vérifier et de valider formellement le comportement et les proprié- tés des services composés obtenus.Cette thèse s’intéresse à la modélisation et à la vérification formelles de la composition de services web décrite avec le standard BPEL en utilisant la méthode B Événementiel. L’approche proposée modélise les parties statique et dynamique de BPEL et se base sur le raffinement pour la structuration du développement d’un processus BPEL. La technique de la preuve de théorèmes est utilisée pour l’établissement des propriétés. Un lien un-à-un est garanti entre les éléments de BPEL et leur correspondant B Evénementiel. Cette correspondance offre une assis- tance aux développeurs pour l’amélioration de la qualité du processus BPEL. Cette approche a été implémentée dans l’outil BPEL2B.

International audience; Output multi-modal human-machine interfaces combine semantically output medias and modalities to increase interaction machine capabilities. In order to provide a rigorous development approach for these interfaces, we have proposed a generic formal model that formally describes the output multi-modal interface construction starting from the information generated by the functional core. This formal model is composed of two sub-models: the first one dedicated to the semantic fission of information and the second one relative to the allocation of modalities and medias for information. This paper presents an Event-B implementation of the semantic fission sub-model.

International audience; Cet article présente un plug-in intégré à la plateforme Rodin implémentant deux approches de formalisation des ontologies décrites par des langages de description des ontologiques (OWL, Plib, ...) en utilisant la théorie des ensembles et la logique du premier ordre supportées par B Événementiel. L’intérêt de cette formalisation est d’enrichir le processus de spécification et de vérification utilisant la méthode B Événementiel, en intégrant des modèles de données et de connaissances décrits dans des ontologies. L’utilisation des ontologies dans un développement B Événementiel va servir à annoter et/ou à typer les données manipulées par le système, ce qui permet de vérifier, en plus des propriétés caractéristiques du système, des propriétés liées à la cohérence des données manipulées et induites par les contraintes du domaine exprimées dans les ontologies.