Search

Your search keyword '"Yamine Aït-Ameur"' showing total 18 results
Start Over Author "Yamine Aït-Ameur" Topic business
18 results on '"Yamine Aït-Ameur"'

1. On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications

Author

Neeraj Kumar Singh, Yamine Aït-Ameur, Philippe Palanque, Romain Geniet, Dominique Méry, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Rennes (UR), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), TELECOM Nancy, Université de Lorraine (UL), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université Toulouse III - Paul Sabatier (UT3), Interactive Critical Systems (IRIT-ICS), ANR-16-CE25-0007,FORMEDICIS,Méthodes formelles pour le développement et l'ingénierie de systèmes interactifs critiques(2016), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
Source code, Correctness, Computer science, media_common.quotation_subject, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], Automotive industry, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 02 engineering and technology, Structuring, Domain (software engineering), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Control theory, 0202 electrical engineering, electronic engineering, information engineering, 0501 psychology and cognitive sciences, MESH: formal method, 050107 human factors, media_common, MESH: MVC, Event (computing), business.industry, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Human-Computer Interaction, MESH: HMI, Scalability, MESH: Event-B, MESH: WIMP, Software engineering, business, Software
Abstract

This paper presents a formal development approach for designing interactive applications using a correct-by-construction approach. In this work, we propose a refinement strategy using model-view-controller (MVC) to structure and design Event-B formal models of the interactive application. The proposed MVC-based refinement strategy facilitates the development of an abstract model and a series of refined models by introducing the possible modes, controller’s behaviour and visual components of the interactive application while preserving the required interaction-related safety properties. To demonstrate the effectiveness, scalability, reliability and feasibility of our approach, we use a small example (from automotive domain) and real-life industrial case studies (from aviation). The entire development is realized in Event-B and the associated Rodin tool is used to analyse and verify the correctness of the formalized model. Finally, the developed Event-B models are used to generate source code using EB2ALL tool for going from the specification to the implementation of the interactive application.

Published
2021
Full Text
View/download PDF

2. Standard Conformance-by-Construction with Event-B

Author

Neeraj Kumar Singh, Dominique Méry, Ismail Mendil, Yamine Aït-Ameur, Philippe Palanque, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Interactive Critical Systems (IRIT-ICS), Alberto Lluch Lafuente, Anastasia Mavridou, TELECOM Nancy, Université de Lorraine (UL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), European Research Consortium for Informatics and Mathematics: ERCIM, Working Group on Formal Methods for Industrial Critical Systems, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and ANR-16-CE25-0007,FORMEDICIS,Méthodes formelles pour le développement et l'ingénierie de systèmes interactifs critiques(2016)

Subjects
Computer science, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Ontology (information science), Data type, Conformance checking, Domain (software engineering), System model, Safety properties, Event-B and Theories, 0202 electrical engineering, electronic engineering, information engineering, Correctness-by-Construction, Standard conformance, ARINC 661, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Critical Interactive Systems, business.industry, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, [INFO.INFO-IA]Computer Science [cs]/Computer Aided Engineering, Formal system, Systems design, 020201 artificial intelligence & image processing, Software engineering, business
Abstract

International audience; Checking the conformance of a system design to a standard is a central activity in the system engineering life cycle, a fortiori when the concerned system is deemed critical. Standard conformance checking entails ensuring that a system or a model of a system faithfully meets the requirements of a specification of a standard improving the robustness and trustworthiness of the system model. In this paper, we present a formal framework based on the correct-by-construction Event-B method and related theories for formally checking the conformance of a formal system model to a formalised standard specification by construction. This framework facilitates the formalization of standard concepts and rules as an ontology, as well as the formalization of an engineering domain, using an Event-B theory consisting of data types and a collection of operators and properties. Conformance checking is accomplished by annotating the system model with typing conditions. We address an industrial case study borrowed from the aircraft cockpit engineering domain to demonstrate the feasibility and strengths of our approach. The ARINC 661 standard is formalised as an Event-B theory. This theory formally models and annotates the safety-critical real-world application of a weather radar system for certification purposes.

Published
2021
Full Text
View/download PDF

3. Towards Leveraging Domain Knowledge in State-Based Formal Methods

Author

Yamine Aït-Ameur, Dominique Méry, Régine Laleau, Neeraj Kumar Singh, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institut National Polytechnique (Toulouse) (Toulouse INP), Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), TELECOM Nancy, Université de Lorraine (UL), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Raschke, Alexander, Riccobene, Elvinia, Schewe, Klaus-Dieter, ANR-13-INSE-0001,IMPEX,Intégration des sémantiques implicite et explicite dans les développements de systèmes discrets fondés sur la preuve.(2013), ANR-17-CE25-0005,DISCONT,Intégration correcte de modèles discrets et continus(2017), ANR-14-CE28-0009,FORMOSE,Méthode outillée de modélisation formelle des exigences pour des systèmes complexes critiques(2014), ANR-19-CE25-0010,EBRP-EventB-Rodin-Plus,Enrichissement de EventB et de RODIN : EventB-Rodin-Plus(2019), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), and Université de Toulouse (UT)

Subjects
business.industry, Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Ontology (information science), Formal methods, Lead (geology), Development (topology), domain knowledge, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Domain knowledge, formal method, State (computer science), ontology, Software engineering, business
Abstract

International audience; System engineering development processes rely on modelling activities that lead to different design models corresponding to different analyses of the system under consideration.

Published
2021
Full Text
View/download PDF

4. Heterogeneous Models and Modelling Approaches for Engineering of Interactive Systems

Author

José Creisssac Campos, Yamine Aït-Ameur, Judy Bowen, Benjamin Weyers, Philippe Palanque, University of Waikato [Hamilton], Universidade do Minho, Interactive Critical Systems (IRIT-ICS), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Universitätsklinikum RWTH Aachen - University Hospital Aachen [Aachen, Germany] (UKA), and RWTH Aachen University

Subjects
Human-Computer Interaction, Interactive computing, [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], ComputingMilieux_THECOMPUTINGPROFESSION, business.industry, Computer science, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Formal methods, Software engineering, business, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Software
Abstract

This editorial introduces the special issue of Interacting with Computer on Heterogeneous Models and Modelling Approaches for Engineering of Interactive Systems. This special issue was proposed to gather the best contributions from a series of workshops organized alongside conferences such as FM’19 (3rd World Congress on Formal Methods) and EICS’19 (11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems). It also encompasses papers submitted directly to this special issue.

Published
2021
Full Text
View/download PDF

5. Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661

Author

Marc Pantel, Neeraj Kumar Singh, Yamine Aït-Ameur, Philippe Palanque, David Navarre, Dominique Méry, Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Université de Lorraine (FRANCE), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Institut National Polytechnique (Toulouse) (Toulouse INP), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), TELECOM Nancy, Université de Lorraine (UL), Interactive Critical Systems (IRIT-ICS), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], Model checking, Computer science, Interface (Java), PetShop, Formal method, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 02 engineering and technology, Interface homme-machine, Domain (software engineering), [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Architectures Matérielles, Validation, 0202 electrical engineering, electronic engineering, information engineering, Génie logiciel, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], Computer-aided software engineering, business.industry, Refinement and proofs, Verification, 020207 software engineering, Human-machine interface (HMI), Animation, Formal methods, Modélisation et simulation, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Systèmes embarqués, ARINC 661, Scalability, Task analysis, Cryptographie et sécurité, Event-B, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, 020201 artificial intelligence & image processing, Software engineering, business
Abstract

International audience; This paper reports our experience for developing Human-Machine Interface (HMI) complying with ARINC 661 specification standard for interactive cockpits applications using formal methods. This development relies on the FLUID modelling language, we have proposed and formally defined in the FORMEDICIS project. FLUID contains essential features required for specifying HMI. To develop the Multi-Purpose Interactive Applications (MPIA) use case, we follow the following steps: an abstract model of MPIA is written using the FLUID language; this MPIA FLUID model is used to produce an Event-B model for checking the functional behaviour, user interactions, safety properties, and interaction related to domain properties; the Event-B model is also used to check temporal properties and possible scenario using the ProB model checker; and finally, the MPIA FLUID model is translated to Interactive Cooperative Objects (ICO) using the PetShop CASE tool to validate the dynamic behaviour, visual properties and task analysis. These steps rely on different tools to check internal consistency along with possible HMI properties. Finally, the formal development of the MPIA case study using FLUID and its embedding into other formal techniques, demonstrates reliability, scalability and feasibility of our approach defined in the FORMEDICIS project.

Published
2020
Full Text
View/download PDF

6. Formal design of scalable conversation protocols using Event‐B: Validation, experiments, and benchmarks

Author

Sarah Benyagoub, Yamine Aït-Ameur, Meriem Ouederni, Atif Mashkoor, and Ahmed Medeghri

Subjects
Formal design, business.industry, Computer science, media_common.quotation_subject, Scalability, Complex system, Conversation, Reuse, Software engineering, business, Software, media_common
Abstract

Contemporary interaction‐based complex systems are often built by reusing existing distributed peers, which have to coordinate with each other to fulfill the client, system, and environmen...

Published
2019
Full Text
View/download PDF

7. Formal Ontology Driven Model Refactoring

Author

Neeraj Kumar Singh, Dominique Méry, Yamine Aït-Ameur, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institut National Polytechnique (Toulouse) (Toulouse INP), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, ANR-13-INSE-0001,IMPEX,Intégration des sémantiques implicite et explicite dans les développements de systèmes discrets fondés sur la preuve.(2013), Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Université de Lorraine (FRANCE), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Ontologies (artificial intelligence), Complex medical case study, Computer science, Large models, 02 engineering and technology, Ontology (information science), computer.software_genre, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Electrocardiography, 0202 electrical engineering, electronic engineering, information engineering, Analytical models, Refactored system model, Refinement and proofs, Refinement-based formal development, Computational modeling, Software maintenance, Modélisation et simulation, Semantics, Formal verification, Refactoring technique, Formal ontology, 010201 computation theory & mathematics, Program verification, Construction approach, Event-B, Complex models, Safety, Domain model, Refactoring, 0102 computer and information sciences, Modelling patterns, Domain (software engineering), maintenance, Formal ontology driven model refactoring, Tools, Formal specification, Safety properties, Ontologies, business.industry, refinement and proofs, 020207 software engineering, Informatique et langage, Do main theories, Complex model, Code refactoring, Software engineering, business, computer, Refactoring, refinement and proofs
Abstract

International audience; Refactoring, successfully used in the field of programming, can be used in maintenance and restructuring of the large and complex models. In this paper, we present a novel approach for model refactoring and a set of modelling patterns that are applicable for refinement-based formal development. In order to carry out this study, we investigate the previously developed large and complex model and required ontology to develop a domain model and a refactored system model. Further, we use the Rodin tools to check the internal consistency with respect to the desired functional behaviour and the required safety properties. Our main contributions are: to develop a refactoring technique related to the \textit{ correct by construction} approach; to use the domain-specific knowledge in a system model explicitly; to define a set of modelling patterns; and to define a restructuring mechanism in the formal development. Finally, this proposed approach is evaluated through a complex medical case study: ECG clinical assessment protocol.

Published
2018
Full Text
View/download PDF

8. Formal Modeling of Cyber-Physical Systems: Lessons Learn from Refinement and Proof Based Methods

Author

Yamine Aït Ameur

Subjects
Focus (computing), Software, Systems theory, Recall, business.industry, Computer science, Hybrid system, Cyber-physical system, Software engineering, business, Control (linguistics), Formal verification
Abstract

Cyber-Physical Systems refer to the tight integration and coordination between computational and physical resources. Modeling their behavior requires handling continuous and discrete behaviors. The definition of the associated models refers to continuous and discrete systems theories. In this talk, we address the problem of designing correct software to control cyber-physical systems. We recall the necessary basic concepts allowing a designer to model such systems. We also give an overview of the different formal approaches supporting the formal verification of these hybrid systems and we highlight the results obtained using these techniques. In particular, we focus on the use of proof and refinement based methods.

Published
2018
Full Text
View/download PDF

9. Web Service Compensation at Runtime: Formal Modeling and Verification Using the Event-B Refinement and Proof Based Formal Method

Author

Yamine Aït-Ameur, Marc Pantel, Guillaume Babin, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, and Institut National Polytechnique (Toulouse) (Toulouse INP)

Subjects
Service (systems architecture), medicine.medical_specialty, Information Systems and Management, Computer Networks and Communications, Computer science, computer.internet_protocol, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, Semantics, 01 natural sciences, Compensation (engineering), 0202 electrical engineering, electronic engineering, information engineering, medicine, [INFO]Computer Science [cs], business.industry, Programming language, 020207 software engineering, Petri net, Formal methods, Computer Science Applications, Business Process Execution Language, 010201 computation theory & mathematics, Hardware and Architecture, Web service, Software engineering, business, computer, Web modeling
Abstract

One of the key interests in web services is the ability to compose them in order to build more powerful and complex ones running in an interoperable and distributed setting. Several languages, like BPEL, that describe such services have been proposed. Similar to the usual complex systems, web service compositions may exhibit inappropriate behaviors in the presence of failures. Compensation mechanisms are available to express running services recovery in case of failures. This paper addresses the problem of the correct design of web service compositions in case of failures. It presents a novel correct-by-construction formal approach based on refinement using the Event-B method. The proposed approach defines a compensation mechanism to repair failed services at runtime. It addresses not only behavioral aspects but also, functional ones through the introduction of repairing invariants whose persistence is enforced during compensation at runtime. Different compensation scenarios and modes are addressed. A formal model for equivalent, degraded and upgraded service compensations relying on the Event-B formalization is defined. The proposal is illustrated on a case study.

Published
2017
Full Text
View/download PDF

10. Strengthening MDE and Formal Design Models by References to Domain Ontologies. A Model Annotation Based Approach

Author

Yamine Aït-Ameur, Kahina Hacid, Systèmes Multi-Agents Coopératifs (IRIT-SMAC), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut National Polytechnique (Toulouse) (Toulouse INP), Institut National Polytechnique de Toulouse - INPT (FRANCE), Centre National de la Recherche Scientifique - CNRS (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), and Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)

Subjects
Computer science, 02 engineering and technology, computer.software_genre, Annotation, Robustness (computer science), MDE Proof and refinement, 0202 electrical engineering, electronic engineering, information engineering, Information system, Model development, Domain ontologies, computer.programming_language, business.industry, 020207 software engineering, Model annotation, Property verification, Domain model, Modélisation et simulation, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Formal design, Event-B, Domain knowledge, 020201 artificial intelligence & image processing, Data mining, Model-driven architecture, Software engineering, business, computer
Abstract

International audience; Critical systems are running in heterogeneous domains. This heterogeneity is rarely considered explicitly when describing and validating processes. Handling explicitly such domain knowledge increases design models robustness due to the expression and validation of new properties mined from the domain models. This paper proposes a stepwise approach to enrich design models describing complex information systems with domain knowledge. We use ontologies to model such domain knowledge. Design models are annotated by references to domain ontologies. The resulting annotated models are checked. It becomes possible to verify domain-related properties and obtain strengthened models. The approach is deployed for two design model development approaches: a Model Driven Engineering (MDE) approach and a correct by construction formal modeling one based on refinement and proof using Event-B method. A case study illustrates both approaches (This work is partially supported by the French ANR-IMPEX project.).

Published
2016
Full Text
View/download PDF

11. Bases de données à base ontologique. Principe et mise en oeuvre

Author

Yamine Aït Ameur, Ladjel Bellatreche, Guy Pierra, and Hondjack Dehainsala

Subjects
Root (linguistics), Information retrieval, Computer science, computer.internet_protocol, business.industry, Ontology (information science), Object (computer science), Model-based reasoning, Strong and weak typing, Type theory, Artificial intelligence, business, computer, XML, Information Systems, Database model
Abstract

In this paper, we propose a new database model called Ontology-Based Database (OBDB) that has two main characteristics. First, it allows to manage both ontologies and data. Second, it permits to associate each data with the ontological concept which defines its meaning. Our approach addresses ontologies expressed as models, i.e. sets of objects that may be accessed from a root object, and that consists of classes and properties. Target data are those data that are instances of ontology classes and that fulfil a strong typing assumption: each instance shall belong to exactly one base class, defined as the lower bound (for the subsumption relationship) of the classes the instance belongs to, and it shall be described only by properties that are applicable to its base class. We first propose an OBDB architecture model, called OntoDB. Then we outline its implementation using the PostgreSQL DBMS, the PLIB ontology model and the EXPRESS language.

Published
2005
Full Text
View/download PDF

12. Thematic Track: Formal Languages and Methods for Designing and Verifying Complex Embedded Systems

Author

Yamine Aït Ameur, Dominique Méry, Virginie Wiels, and Frédéric Boniol

Subjects
business.industry, Computer science, Programming language, Object language, ComputerApplications_COMPUTERSINOTHERSYSTEMS, Avionics, Grammar systems theory, Formal methods, computer.software_genre, Formal specification, Formal language, Systems engineering, Aerospace, business, Formal verification, computer
Abstract

Nowadays, it is well accepted that the develop- ment of critical systems involves the use of formal methods. One of the major fields where these methods made a lot of progress are the avionics, aerospace, transport areas, telecom, etc. These systems are responsible for various functions, such as navigation, guidance, stability, power management, board/ground communications, passenger entertainment.... Moreover, their complexity is continuously growing.

Published
2010
Full Text
View/download PDF

13. A generic formal model for fission of modalities in output multi–modal interactive systems

Author

Yamine Aït Ameur, Mohamed Ahmed Nacer, and Linda Mohand Oussaïd

Subjects
Modalities, Modal, Theoretical computer science, Formal design, Computer science, business.industry, Robustness (computer science), Formal specification, Usability, business, Design space, Formal verification
Abstract

Output multi-modal human-machine interfaces combine semantically output medias and modalities in order to increase interaction machine capabilities. The aim of this paper is to present a formal model supporting formal specifications of output multi-modal interactive systems. As a consequence, the expected usability and robustness properties can be expressed and checked. This paper proposes a generic model which permits to specify the output multimodal interfaces following the CASE design space.

Published
2009
Full Text
View/download PDF

14. PLIB Ontology: A Mature Solution for Products Characterization in B2B Electronic Commerce

Author

Yamine Aït Ameur, Habiba Drias, Guy Pierra, Youcef Aklouf, Laboratoire d'Informatique Scientifique et Industrielle (LISI), Université de Poitiers-Ecole Nationale Supérieure de Mécanique et d'Aérotechnique [Poitiers] (ISAE-ENSMA), Laboratoire de Recherche en Intelligence Artificielle [Alger] (LRIA), and Université des Sciences et de la Technologie Houari Boumediene [Alger] (USTHB)

Subjects
021103 operations research, Knowledge management, business.industry, Computer science, Business process, Interoperability, 0211 other engineering and technologies, 020207 software engineering, 02 engineering and technology, computer.file_format, Business-to-business, Ontology (information science), Computer Science Applications, Business process management, ebXML, Management of Technology and Innovation, 0202 electrical engineering, electronic engineering, information engineering, Business logic, [INFO]Computer Science [cs], Layer (object-oriented design), business, Software engineering, computer
Abstract

This paper deals with the integration of PLIB ontologies in electronic commerce architectures, especially in B2B electronic commerce. Exchange of data, information, and knowledge is the key issue. To ensure reliability and feasibility of such exchange, two kinds of ontologies prove useful. One addresses products and services characterization, whereas the other addresses business processes. This paper aims to demonstrate the capability of integration of these two kinds of ontologies in a unique and global B2B-layered architecture. The orthogonality principle is applied. It allows the use of any best existing standard in both business layer and contents layer. In this paper, we use RosettaNet PIPs and ebXML in the business process layer, and we claim that PLIB ontologies are the best-in-class solution for the contents layer. These standards are used conjointly to promote interoperability and automation between partners involved in exchange. The originality of our approach is the possibility offered to the partners to use any defined business process with any defined content. A case study showing an application of such ontologies using RosettaNet PIP2A9 for business process and PLIB-based ontology for product characterization is presented. Implementation issues are also discussed.

Published
2005
Full Text
View/download PDF

15. Representation of Procedural Knowledge and its Use to Compute a Form of Subsumption

Author

Yamine Aït Ameur

Subjects
Knowledge-based systems, Computer science, business.industry, Representation (systemics), Computer Science::Programming Languages, Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), Artificial intelligence, computer.software_genre, Procedural knowledge, business, computer, Uniform representation, Natural language processing
Abstract

This paper shows the possibility to describe language based epresentations by model based representations. This uniform representation is useful for model integrations and helps to compute a form of subsumption.

Published
2004
Full Text
View/download PDF

16. Interactive System Safety and Usability Enforced with the Development Process

Author

Patrick Girard, Yamine Aït Ameur, and Francis Jambon

Subjects
Engineering, business.industry, Heuristic evaluation, Systems engineering, Usability inspection, Usability, System safety, User interface, business, Software architecture, Software engineering, Formal methods, Component-based usability testing
Abstract

This paper introduces a new technique for the verification of both safety and usability requirements for safety-critical interactive systems. This technique uses the model-oriented formal method B and makes use of an hybrid version of the MVC and PAC software architecture models. Our claim is that this technique -that uses proofs obligations- can ensure both usability and safety requirements, from the specification step of the development process, to the implementation. This technique is illustrated by a case study: a simplified user interface for a Full Authority Digital Engine Control (FADEC) of a single turbojet engine aircraft.

Published
2001
Full Text
View/download PDF

17. Cooperation of Formal Methods in an Engineering Based Software Development Process

Author

Yamine Aït Ameur

Subjects
business.industry, Computer science, Software development, Software requirements specification, Formal methods, Software development process, Software, Application domain, Formal specification, Goal-Driven Software Development Process, Artificial intelligence, Software verification and validation, Software engineering, business, Formal verification, Software verification
Abstract

This paper presents a global development approach for using different formal techniques in a common software development. The underlying methodology is based on the identification, formalization and verification of the properties, of the system to be developed, expressed in the requirements. The approach we suggest consists in identifying a main formal technique to support the whole system specification at an abstract level and one or several secondary techniques that prove efficient for parts of the development. This approach has been put into practice in different and distant application domains. The considered application domain covered by this paper is human-computer interaction software.

Published
2000
Full Text
View/download PDF

18. Multi-level Networked Knowledge Base: DDL-Reasoning

Author

Mohamed Tarek Khadir, Antoine Zimmermann, Sihem Klai, Département Informatique pour les Systèmes Coopératifs Ouverts et Décentralisés (ISCOD-ENSMSE), École des Mines de Saint-Étienne (Mines Saint-Étienne MSE), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut Henri Fayol, Laboratoire Hubert Curien [Saint Etienne] (LHC), Institut d'Optique Graduate School (IOGS)-Université Jean Monnet [Saint-Étienne] (UJM)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Gestion Electronique de Documents (LabGED), Université de Annaba, Ladjel Bellatreche, Óscar Pastor, Jesús M. Almendros Jiménez, and Yamine Aït-Ameur

Subjects
Theoretical computer science, Computer science, business.industry, Multi-level networked knowledge base, 02 engineering and technology, Ontology (information science), Contextual reasoning, computer.software_genre, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Formalism (philosophy of mathematics), Knowledge base, 020204 information systems, Ontology components, 0202 electrical engineering, electronic engineering, information engineering, Ontologies, DDL-reasoning, 020201 artificial intelligence & image processing, Data mining, Ontology-alignment, Equivalence (formal languages), business, Ontology alignment, computer
Abstract

International audience; This paper describes a new formalism based on multi-level networked knowledge (MLNK), a combination of different ontologies describing heterogeneous and complementary domains aligned with semantic correspondences. Ontology alignments make explicit the correspondences between terms from different ontologies and must be taken into account in reasoning, where two explicit form of correspondences are given: mappings represent predefined relations such as subsumption, equivalence, or disjointness, that have a fixed semantics in all interpretations; as well as links that can relate complementary ontologies by introducing terms defined by experts, and their semantics varies according to interpretations. The proposed MLNK formalism can be transformed into a Distributed System capable of supporting DDL semantics. It permits to apply a contextual reasoning where ontologies and alignments by pairs of ontologies are developed in different and incompatible contexts. The semantic of the proposed formalism is extensively described along with an illustrative example.

Published
2016
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results