Search

Your search keyword '"Université Abdelhamid Ibn Badis Mostaganem (ALGERIE)"' showing total 3 results
Start Over Author "Université Abdelhamid Ibn Badis Mostaganem (ALGERIE)"
3 results on '"Université Abdelhamid Ibn Badis Mostaganem (ALGERIE)"'

1. Incremental Construction of Realizable Choreographies

Author

Yamine Aït-Ameur, Meriem Ouederni, Atif Mashkoor, Sarah Benyagoub, Université Abdelhamid Ibn Badis de Mostaganem, 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), Johannes Kepler University Linz [Linz] (JKU), Software Competence Center Hagenberg (SCCH), Johannes Kepler Universität Linz (JKU), Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - INPT (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Linz Johannes Kepler University (AUSTRIA), Université Abdelhamid Ibn Badis Mostaganem (ALGERIE), Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France), Software Competence Center Hagenberg - SCCH (Hagenberg, Autriche), and Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)

Subjects
Theoretical computer science, Realisability, Computer science, media_common.quotation_subject, 020207 software engineering, 02 engineering and technology, Modélisation et simulation, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Set (abstract data type), Constructed language, Conversation protocols, Asynchronous communication, Scalability, 0202 electrical engineering, electronic engineering, information engineering, Event-B, 020201 artificial intelligence & image processing, Conversation, Correct-by-construction method proof and refinement, media_common
Abstract

International audience; This paper proposes a correct-by-construction method to build realizable choreographies described using conversation protocols (CPs). We define a new language consisting of an operators set for incremental construction of CPs. We suggest an asynchronous model described with the Event-B method and its refinement strategy, ensuring the scalability of our approach.

Published
2018

2. Towards correct Evolution of Conversation Protocols

Author

Benyagoub, Sarah, Ouederni, Meriem, Aït-Ameur, Yamine, 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é Abdelhamid Ibn Badis Mostaganem (ALGERIE), Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France), and Institut National Polytechnique de Toulouse - INPT (FRANCE)

Subjects
Realisability, Behavioural Systems, Systèmes embarqués, Interface homme-machine, System Evolution, Formal Verification, Conversation Protocols
Abstract

Distributed software systems change dynamically due to the evolution of their environment and/or requirements, their internal designing policies, and/or their specification bugs which must be fixed. Hence, checking system changes must be run continuously. Such systems are usually composed of distributed software entities (called peers) interacting with each other through message exchanges, and this is to fulfil a common goal. The goal is often specified by a conversation protocol (CP), i.e. sequences of sent messages. If there exists a set of peers implementing CP, then CP is said to be realisable. In this paper, we propose a stepwise approach for checking whether an evolution, i.e. adding and/or removing messages and/or peers, can be applied to a CP that was realisable before updating it.We define a set of correct evolution patterns and we suggest an algebra of CP evolution. Our approach ensures that CP evolution preserves the realisability condition.

Published
2016

3. Correct-by-Construction Evolution of Realisable Conversation Protocols

Author

Yamine Ait-Ameur, Neeraj Kumar Singh, Sarah Benyagoub, Meriem Ouederni, 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é Abdelhamid Ibn Badis Mostaganem (ALGERIE), Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France), Université Abdelhamid Ibn Badis de Mostaganem, 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é Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-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é Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées, 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), and Institut National Polytechnique (Toulouse) (Toulouse INP)

Subjects
Correct-by-Construction, Realisability, Computer science, media_common.quotation_subject, Existential quantification, 02 engineering and technology, computer.software_genre, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Set (abstract data type), Correct-by-construction method, Development (topology), 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Conversation, Control (linguistics), Proof and refinement, Formal verification, Protocol (object-oriented programming), media_common, Programming language, Theorem Proving, Informatique et langage, 020207 software engineering, Refinement, Modélisation et simulation, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Automated theorem proving, Conversation protocols, System evolution, Event-B, computer, System Evolution, Realisability, Conversation Protocols, Formal Verification, Correct-by-Construction, Theorem Proving, Refinement, Event-B
Abstract

International audience; Distributed software systems are often built by composing independent and autonomous peers with cross-organisational interaction and no centralised control. These peers can be administrated and executed by geographically distributed and autonomous companies. In a top-down design of distributed software systems, the peers' interaction is often described by a global specification called Conversation Protocol (CP) and one have to check its realisability i.e., whether there exists a set of peers implementing this CP. In dynamic environments, CP needs to be updated wrt. new environment changes and end-user interaction requirements. This paper tackles CP evolution such that its realisability must be preserved. We define some evolution patterns and prove that they ensure the realisability. We also show how our proposal can be supported by existing methods and tools based on refinement and theorem proving, using the event-B langage and RODIN development tools.

Published
2016

Catalog

Books, media, physical & digital resources
See catalog results