1. Correctness by construction and style preserving reconfigurations of system of systems
- Author
-
Cédric Eichler, Khalil Drira, Thierry Monteil, Patricia Stolf, Sécurité des Données et des Systèmes (SDS), Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Université d'Orléans (UO)-Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université d'Orléans (UO)-Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA), Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL), Institut National des Sciences Appliquées (INSA), Équipe Services et Architectures pour Réseaux Avancés (LAAS-SARA), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-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)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Système d’exploitation, systèmes répartis, de l’intergiciel à l’architecture (IRIT-SEPIA), Institut de recherche en informatique de Toulouse (IRIT), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), 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é Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), 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)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), 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), Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Institut National des Sciences Appliquées de Toulouse - INSA (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Institut National des Sciences Appliquées de Centre Val de Loire - INSA (FRANCE), Université d'Orléans (FRANCE), Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse 1 Capitole (UT1)-Université Toulouse - Jean Jaurès (UT2J)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse 1 Capitole (UT1)-Université Toulouse - Jean Jaurès (UT2J), 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), and Institut National Polytechnique de Toulouse - INPT (FRANCE)
- Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] ,Model checking ,Theoretical computer science ,Correctness ,Computer science ,Système d'exploitation ,Réseaux et télécommunications ,02 engineering and technology ,Mathematical proof ,[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] ,Architectures Matérielles ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Formalisms ,Theory of computation ,System of systems ,Graph rewriting ,020207 software engineering ,Systèmes embarqués ,Graph ,Rewrite systems ,Calcul parallèle, distribué et partagé ,Grammars and context-free languages ,Scalability ,Formal languages and automata theory ,Graph (abstract data type) ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,[INFO.INFO-OS]Computer Science [cs]/Operating Systems [cs.OS] ,[INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC] - Abstract
International audience; In distributed systems and dynamic environments, software architectures may evolve. A crucial issue when conducting system evolutions is to maintain the system in a consistent and functional state. As system complexity rises, manual checking or exhaustive model checking may be too time- and resource-consuming, lacking in scalability. This is particularly true with system of systems. Based on formal proofs in design-time, correctness by construction has recently emerged to efficiently guarantee system coherency.This article proposes a new method for the construction and specification of correct by construction system reconfigurations. Such transformations are characterized by graph rewriting rules that necessarily preserve the coherency of a system. We firstly propose operators on graph transformations and show that they conserve their correctness. Given a system specified by a graph grammar, these operators can be leveraged to construct correct transformations. We show in particular that any correct configuration can be reached starting from any other one without inconsistent intermediate step, using such transformations only.
- Published
- 2018
- Full Text
- View/download PDF