Search

Your search keyword '"Karine Altisen"' showing total 58 results
Start Over Author "Karine Altisen" Database OpenAIRE
58 results on '"Karine Altisen"'

1. <scp>sasa</scp>: a SimulAtor of Self-stabilizing Algorithms

Author

Karine Altisen, Stéphane Devismes, and Erwan Jahier

Subjects
General Computer Science
Abstract

In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model (also called the locally shared memory model with composite atomicity). This model is the most commonly used one in the self-stabilizing area to prove both the correct operation of self-stabilizing algorithms and complexity bounds on them. sasa encompasses all features necessary to debug, test and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Properties of algorithms can be checked using formal test oracles. The sasa distribution also provides several facilities to easily achieve (batch-mode) simulation campaigns. We show that the lightweight design of sasa allows to efficiently perform huge such campaigns. Following a modular approach, we have aimed at relying as much as possible the design of sasa on existing tools, including ocaml, dot and several tools developed in the Synchrone Group of the VERIMAG laboratory.

Published
2022
Full Text
View/download PDF

2. Certification of an exact worst-case self-stabilization time

Author

Karine Altisen, Pierre Corbineau, Stéphane Devismes, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Modélisation, Information et Systèmes - UR UPJV 4290 (MIS), and Université de Picardie Jules Verne (UPJV)

Subjects
Discrete mathematics, Correctness, General Computer Science, Computer science, Liveness, Proof assistant, 020207 software engineering, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Upper and lower bounds, Theoretical Computer Science, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], 010201 computation theory & mathematics, Distributed algorithm, 0202 electrical engineering, electronic engineering, information engineering, Dijkstra's algorithm, Time complexity
Abstract

Unlike qualitative properties such as correctness (safety and liveness), quantitative properties of distributed algorithms have only been certified in very few works. This work is the first attempt to certify time complexity bounds of fault-tolerant distributed algorithms. Our case study consists in formally proving, using the Coq proof assistant, the time complexity of the first Dijkstra’s self-stabilizing token ring algorithm. In more detail, we formally prove both the self-stabilization and exact worst-case stabilization time of this algorithm assuming fully asynchronous settings. This latter result is obtained in two main steps. First, we certify a non-trivial upper bound on the stabilization time, i.e., every execution contains at most steps, where N is the number of nodes. Then, we exhibit, for every ring of at least four nodes, a possible execution whose complexity exactly matches that upper bound. Notice that this tight bound was unknown until now, even among self-stabilization researchers.

Published
2022
Full Text
View/download PDF

3. Introduction to Distributed Self-Stabilizing Algorithms

Author

Karine Altisen, Stéphane Devismes, Swan Dubois, and Franck Petit

Subjects
010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences
Published
2019
Full Text
View/download PDF

4. Election in unidirectional rings with homonyms

Author

Karine Altisen, Lawrence L. Larmore, Anaïs Durand, Stéphane Devismes, Ajoy K. Datta, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Department of Computer Science [Las Vegas], University of Nevada [Las Vegas] (WGU Nevada), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), and ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016)

Subjects
Leader election, Computer Networks and Communications, Computer science, Unidirectional Rings, 020206 networking & telecommunications, 02 engineering and technology, Homonyms, Theoretical Computer Science, Combinatorics, Multiplicity, Artificial Intelligence, Hardware and Architecture, Bounded function, 0202 electrical engineering, electronic engineering, information engineering, Leader Election, 020201 artificial intelligence & image processing, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Software
Abstract

International audience; We study leader election in unidirectional rings of homonyms that have no a priori knowledge of the number of processes. In this context, we show that there exists no algorithm that solves the process-terminating leader election problem for the class of asymmetrically labeled unidirectional rings. More precisely, we prove that there is no process-terminating leader election algorithm even for the subclass of unidirectional rings where at least one label is unique. Message-terminating leader election is also impossible for the class of unidirectional rings where only a bound on multiplicity is known. However, we show that the processterminating leader election is possible for two particular subclasses of asymmetrically labeled unidirectional rings where the multiplicity is bounded. We propose three efficient algorithms and analyze their complexities. We also give some non-trivial lower bounds.

Published
2020
Full Text
View/download PDF

5. Brief Announcement: Self-stabilizing Systems in Spite of High Dynamics

Author

Franck Petit, Colette Johnen, Karine Altisen, Stéphane Devismes, Anaïs Durand, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), This study was partially supported by the French ANR projects ANR-16-CE40-0023 (DESCARTES) and ANR-16CE25-0009-03 (ESTATE)., ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])

Subjects
Discrete mathematics, Class (set theory), Leader election, Computer science, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Time-varying graphs, 010201 computation theory & mathematics, Bounded function, 0202 electrical engineering, electronic engineering, information engineering, Spite, 020201 artificial intelligence & image processing, Speculation, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
Abstract

International audience; We initiate research on self-stabilization in highly dynamic identified message-passing systems where dynamics is modeled using time-varying graphs (TVGs). More precisely, we address the self-stabilizing leader election problem in three wide classes of TVGs: the class $TC^B(∆)$ of TVGs with temporal diameter bounded by $∆$, the class $TC^Q(∆)$ of TVGs with temporal diameter quasi-bounded by $∆$, and the class $TC^R$ of TVGs with recurrent connectivity only, where TC^B(∆) ⊆ $TC^Q(∆) ⊆ TC^R$. We first study conditions under which our problem can be solved. Precisely, we introduce the notion of size-ambiguity to show that the assumption on the knowledge of the number n of processes is central. Our results reveal that, despite the existence of unique process identifiers, any deterministic self-stabilizing leader election algorithm working in the TVG class $TC^Q(∆)$ or $TC^R$ cannot be size-ambiguous, justifying why our solutions for those classes assume the exact knowledge of n. We then present three self-stabilizing leader election algorithms for the TVG classes $TC^B(∆)$, $TC^Q(∆)$, and $TC^R$, respectively.

Published
2020
Full Text
View/download PDF

6. sasa: A SimulAtor of Self-stabilizing Algorithms

Author

Stéphane Devismes, Karine Altisen, Erwan Jahier, Jahier, Erwan, Abstraction modulaire pour le calcul distribué - - DESCARTES2016 - ANR-16-CE40-0023 - AAPG2016 - VALID, Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps - - ESTATE2016 - ANR-16-CE25-0009 - AAPG2016 - VALID, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), and ANR-16-CE25-0009-03,ESTATE,Enhancing Safety and self-STabilization in Time-varying distributed Environments(2016)

Subjects
050101 languages & linguistics, dis- tributed computing, Computer science, media_common.quotation_subject, reactive programs, Self-stabilization, 02 engineering and technology, Faithful representation, distributed computing, Sasa, synchronous languages, [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], 0202 electrical engineering, electronic engineering, information engineering, 0501 psychology and cognitive sciences, Transient (computer programming), Simulation, media_common, atomic-state model, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], biology, 05 social sciences, simulation, biology.organism_classification, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, debugging, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], self-stabilization, Debugging, Distributed algorithm, 020201 artificial intelligence & image processing, [INFO.INFO-MO] Computer Science [cs]/Modeling and Simulation, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Algorithm
Abstract

International audience; We present SASA, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. SASA is implemented as a faithful representation of the atomic-state model. This model is the most commonly used in the self-stabilizing area to prove both the correct operation and complexity bounds of self-stabilizing algorithms. SASA encompasses all features necessary to debug, test, and analyze self-stabilizing algorithms. Algorithm's properties can be checked using formal test oracles. Asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators.

Published
2020
Full Text
View/download PDF

7. On probabilistic snap-stabilization

Author

Karine Altisen and Stéphane Devismes

Subjects
020203 distributed computing, Leader election, Theoretical computer science, Property (philosophy), General Computer Science, Liveness, Probabilistic logic, Process (computing), 0102 computer and information sciences, 02 engineering and technology, Fault (power engineering), 01 natural sciences, Theoretical Computer Science, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Probabilistic analysis of algorithms, Almost surely, Mathematics
Abstract

In this paper, we introduce probabilistic snap-stabilization. We relax the definition of deterministic snap-stabilization without compromising its safety guarantees. In an unsafe environment, a probabilistically snap-stabilizing algorithm satisfies its safety property immediately after the last fault; whereas its liveness property is only ensured with probability 1. We show that probabilistic snap-stabilization is more expressive than its deterministic counterpart. Indeed, we propose two probabilistic snap-stabilizing algorithms for a problem having no deterministic snap- or self-stabilizing solution: guaranteed service leader election in arbitrary anonymous networks. This problem consists in computing a correct answer to each process that initiates the question “Am I the leader of the network?,” i.e., (1) processes always compute the same answer to that question and (2) exactly one process computes the answer true. Our solutions being probabilistically snap-stabilizing, the answers are only delivered within an almost surely finite time; however any delivered answer is correct, regardless the arbitrary initial configuration and provided the question has been properly started.

Published
2017
Full Text
View/download PDF

8. Squeezing Streams and Composition of Self-stabilizing Algorithms

Author

Pierre Corbineau, Karine Altisen, Stéphane Devismes, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Jorge A. Pérez, Nobuko Yoshida, TC 6, and WG 6.1

Subjects
Correctness, Distributed algorithm, Computer science, Composition operator, Proof assistant, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, Function (mathematics), 01 natural sciences, Formal proof, Image (mathematics), Coq proof assistant, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], 020401 chemical engineering, 010201 computation theory & mathematics, Streams, Coinduction, [INFO]Computer Science [cs], 0204 chemical engineering, Algorithm, Composition
Abstract

Part 1: Full Papers; International audience; Composition is a fundamental tool when dealing with complex systems. We study the hierarchical collateral composition which is used to combine self-stabilizing distributed algorithms. The PADEC library is a framework developed with the Coq proof assistant and dedicated to the certification of self-stabilizing algorithms. We enrich PADEC with the composition operator and a sufficient condition to show its correctness. The formal proof of the condition leads us to develop new tools and methods on potentially infinite streams, these latter ones being used to model the algorithms’ executions. The cornerstone has been the definition of the function which removes duplicates from streams.

Published
2019
Full Text
View/download PDF

11. Silence dans la forêt !

Author

Karine Altisen, Stéphane Devismes, Anaïs Durand, Devismes, Stéphane, Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps - - ESTATE2016 - ANR-16-CE25-0009 - AAPG2016 - VALID, Abstraction modulaire pour le calcul distribué - - DESCARTES2016 - ANR-16-CE40-0023 - AAPG2016 - VALID, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016), and CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI], Autostabilisation, Forêts, [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Silence, Arbres
Abstract

International audience; Nous formalisons des schémas d'algorithmes distribués, classiquement utilisés en autostabilisation, afin d'obtenir des résultats généraux relatifs à leur correction et leur complexité. Précisément, nous étudions une classe d'algorithmes dédiés aux réseaux munis d'un sens de direction décrivant une forêt couvrante. La définition de cette classe est simple au sens où elle est quasi-syntaxique. Tous les algorithmes de cette classe sont (1) autostabilisants et silencieux, et (2) ont un temps de stabilisation à la fois polynomial en mouvements et asymptotiquement optimal en rondes. Pour illustrer la polyvalence de notre méthode, nous passons en revue plusieurs travaux où nos résultats s'appliquent.

Published
2019

17. Gradual stabilization

Author

Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit, École nationale supérieure d'informatique et de mathématiques appliquées (ENSIMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), This study has been partially supported by the anr projects Descartes, France (ANR-16-CE40-0023) and Estate, France (ANR-16-CE25-0009)., ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), and Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
Computer Networks and Communications, Superstabilization, Unison, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Theoretical Computer Science, Synchronization problems, Gradual stabilization, 010201 computation theory & mathematics, Artificial Intelligence, Hardware and Architecture, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Safe-convergence, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Software, ComputingMilieux_MISCELLANEOUS, Self-stabilization
Abstract

International audience

Published
2019
Full Text
View/download PDF

19. Stabilisation progressive

Author

Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Technion - Israel Institute of Technology [Haifa], DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, and Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Unisson, Autostabilisation, Réseaux dynamiques, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
Abstract

International audience; Cet article est un résumé étendu de (Altisen et al., Euro-Par 2016) dans lequel nous nous intéressons à des réseaux pouvant subir des changements topologiques transitoires. Nous proposons une nouvelle spécialisation de l'autostabilisation adaptée à ce type de réseau : la stabilisation progressive. Un algorithme est progressivement stabilisant sous hypothèse de (τ, ρ)-dynamicité s'il est autostabilisant et satisfait la propriété supplémentaire suivante : après au plus τ pas dynamiques vérifiant la condition ρ et se produisant à partir d'une configuration légitime, l'algorithme converge rapidement vers une configuration où une spécification plus faible est satisfaite ; puis il continue à converger progressivement vers des configurations où des spécifications de plus en plus fortes sont vérifiées, et ce, jusqu'à retrouver une configuration légitime vérifiant la spécification initiale du problème. Nous illustrons cette nouvelle propriété en proposant un algorithme progressivement stabilisant de synchronisation d'horloges.

Published
2018

20. Eviter les collisions dans les réseaux 6TiSCH

Author

Olivier Alphand, Karine Altisen, Rodolphe Bertolini, Stéphane Devismes, Ali Fahs, Franck Rousseau, Drakkar, Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Laboratoire d'Informatique de Grenoble (LIG), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), SYNCHRONE, Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Université Grenoble Alpes (UGA), and ANR-11-LABX-0025-01,PERSYVAL-lab,Systèmes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011)

Subjects
IoT, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Scheduling Functions, IEEE802154e, TSCH, 6top, 6TiSCH
Abstract

National audience; Les réseaux multi-sauts 802.15.4e TSCH s'appuient sur des échéanciers de communication efficaces. Notre solution complète les algorithmes de construction de tels échéanciers en limitant la réutilisation de cellules temps-fréquence déjà utilisées par des noeuds voisins. Nos simulations montrent un gain significatif par rapport à l'existant.

Published
2018

21. Acyclic Strategy for Silent Self-Stabilization in Spanning Forests

Author

Stéphane Devismes, Karine Altisen, Anaïs Durand, SYNCHRONE, VERIMAG ( VERIMAG - IMAG ), Université Joseph Fourier - Grenoble 1 ( UJF ) -Institut National Polytechnique de Grenoble ( INPG ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Grenoble Alpes ( UGA ) -Université Joseph Fourier - Grenoble 1 ( UJF ) -Institut National Polytechnique de Grenoble ( INPG ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Grenoble Alpes ( UGA ), Université Grenoble Alpes [Saint Martin d'Hères], VERIMAG UMR 5104, Université Grenoble Alpes, France, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), the World Is Distributed Exploring the tension between scale and coordination (WIDE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), ANR-16-CE40-0023,DESCARTES,Abstraction modulaire pour le calcul distribué(2016), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and Université Grenoble Alpes [2016-2019] (UGA [2016-2019])

Subjects
FOS: Computer and information sciences, Class (set theory), Polynomial, Correctness, Theoretical computer science, Computer science, [ INFO.INFO-NI ] Computer Science [cs]/Networking and Internet Architecture [cs.NI], Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Simple (abstract algebra), 0202 electrical engineering, electronic engineering, information engineering, tree networks, Time complexity, bottom-up actions, top-down actions, Asymptotically optimal algorithm, Computer Science - Distributed, Parallel, and Cluster Computing, 010201 computation theory & mathematics, silence, C.2.4 Distributed Systems, 020201 artificial intelligence & image processing, Distributed, Parallel, and Cluster Computing (cs.DC), [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Daemon
Abstract

In this paper, we formalize design patterns, commonly used in the self-stabilizing area, to obtain general statements regarding both correctness and time complexity guarantees. Precisely, we study a general class of algorithms designed for networks endowed with a sense of direction describing a spanning forest (e.g., a directed tree or a network where a directed spanning tree is available) whose characterization is a simple (i.e., quasi-syntactic) condition. We show that any algorithm of this class is (1) silent and self-stabilizing under the distributed unfair daemon, and (2) has a stabilization time which is polynomial in moves and asymptotically optimal in rounds. To illustrate the versatility of our method, we review several existing works where our results apply.

Published
2018
Full Text
View/download PDF

22. Collision Prevention in Distributed 6TiSCH Networks

Author

Ali J. Fahs, Olivier Alphand, Franck Rousseau, Stéphane Devismes, Rodolphe Bertolini, Karine Altisen, VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Drakkar, Laboratoire d'Informatique de Grenoble (LIG), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), ANR-11-LABX-0025-01,PERSYVAL-lab,Systèmes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), ANR-13-INFR-0008,DataTweet,DataTweet - un service public de communications opportunistes(2013), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), and ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011)

Subjects
IoT, business.industry, Computer science, 6top, 010401 analytical chemistry, Mobile computing, 020206 networking & telecommunications, Access control, 02 engineering and technology, Reuse, 01 natural sciences, 0104 chemical sciences, Scheduling (computing), [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], IEEE802154e, Scheduling Functions, Collision prevention, TSCH, 0202 electrical engineering, electronic engineering, information engineering, Wireless, 6TiSCH, business, Internet of Things, Wireless sensor network, Computer network
Abstract

International audience; —The IEEE802.15.4e standard for low power wireless sensor networks defines a new mode called Time Slotted Channel Hopping (TSCH) as Medium Access Control (MAC). TSCH allows highly efficient deterministic time-frequency schedules that are built and maintained by the 6TiSCH operation sublayer (6top). In this paper, we propose a solution to limit the allocation of identical cells to co-located pair of nodes by distributed TSCH scheduling algorithms. It consists of making nodes able to overhear past cell negotiations exchanged in shared cells by their neighbors and prevent the nodes from reusing already assigned cells in future allocations. Our mechanism has been tested through simulations that show a significant improvement with respect to random scheduling algorithms.

Published
2017
Full Text
View/download PDF

23. SR3: secure resilient reputation-based routing

Author

Pascal Lafourcade, Stéphane Devismes, Karine Altisen, Raphaël Jamet, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), SYNCHRONE, Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Routing protocol, Dynamic Source Routing, Equal-cost multi-path routing, Computer Networks and Communications, Computer science, Routing table, media_common.quotation_subject, 02 engineering and technology, security, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, Electrical and Electronic Engineering, media_common, Static routing, Cryptographic primitive, business.industry, Policy-based routing, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, 020206 networking & telecommunications, resiliency, 020202 computer hardware & architecture, Link-state routing protocol, routing, Multipath routing, 020201 artificial intelligence & image processing, Routing (electronic design automation), Index Terms—Wireless sensor networks, business, Wireless sensor network, Information Systems, Computer network, Reputation
Abstract

International audience; In this paper, we propose SR3 (which means Secure Resilient Reputation-based Routing), a secure and resilient algorithm for convergecast routing in WSNs (Wireless Sensor Networks). SR3 uses lightweight cryptographic primitives to achieve data confidentiality and unforgeability. Security of SR3 has been proven formally using two verification tools: CryptoVerif and Scyther. We made simulations to show the resiliency of SR3 against various scenarios, where we mixed selective forwarding, blackhole, wormhole, and Sybil attacks. We compared our solution to several routing algorithms of the literature. Our results show that the resiliency accomplished by SR3 is drastically better than the one achieved by those protocols, especially when the network is sparse. Moreover, unlike previous solutions , SR3 self-adapts after compromised nodes suddenly change their behavior.

Published
2017
Full Text
View/download PDF

24. Leader Election in Asymmetric Labeled Unidirectional Rings

Author

Lawrence L. Larmore, Ajoy K. Datta, Stéphane Devismes, Karine Altisen, and Anaïs Durand

Subjects
Leader election, Theoretical computer science, Computer science, 020206 networking & telecommunications, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Upper and lower bounds, Combinatorics, 010201 computation theory & mathematics, Distributed algorithm, Bounded function, 0202 electrical engineering, electronic engineering, information engineering, Algorithm design, Time complexity
Abstract

We study (deterministic) leader election in unidirectional rings of homonym processes that have no a priori knowledge on the number of processes. In this context, we show that there is no algorithm that solves process-terminating leader election for the class of asymmetric labeled rings. In particular, there is no process-terminating leader election algorithm in rings in which at least one label is unique. However, we show that process-terminating leader election is possible for the subclass of asymmetric rings, where multiplicity is bounded. We confirm this positive results by proposing two algorithms, which achieve the classical trade-off between time and space.

Published
2017
Full Text
View/download PDF

25. Concurrence et allocation de ressources locales instantanément stabilisante

Author

Karine Altisen, Stéphane Devismes, Anaïs Durand, SYNCHRONE, VERIMAG (VERIMAG - IMAG), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Allocation de ressources locales, Stabilisation instantanée, Concurrence, Algorithmes distribués
Abstract

International audience; Cet article est un résumé de (Altisen et al., 2015) où nous étudions la notion de concurrence dans les problèmes d'allocation de ressources. Nous proposons des propriétés générales permettant d'exprimer la qualité de concurrence d'une solution à un problème d'allocation de ressources et établissons quelle qualité de concurrence peut être atteinte par un algorithme résolvant le problème d'allocation de ressources locales. Enfin, nous proposons un algorithme d'allocation de ressources locales instantanément stabilisant qui réalise cette qualité de concurrence.

Published
2016

26. A Framework for Certified Self-Stabilization

Author

Pierre Corbineau, Karine Altisen, Stéphane Devismes, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), VERIMAG UMR 5104, Université Grenoble Alpes, France, Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Elvira Albert, Ivan Lanese, TC 6, and WG 6.1

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Property (programming), Computer science, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, Certification, Mathematical proof, 01 natural sciences, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], Cardinality, Dominating set, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Coq, [INFO]Computer Science [cs], Proof assistant, Discrete mathematics, Atomicity, 020207 software engineering, Silent algorithms, Logic in Computer Science (cs.LO), Potential functions, Computer Science - Distributed, Parallel, and Cluster Computing, 010201 computation theory & mathematics, Computer Science::Mathematical Software, Distributed, Parallel, and Cluster Computing (cs.DC)
Abstract

We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity, the most commonly used model in the self-stabilizing area. We then validate our framework by certifying a non trivial part of an existing silent self-stabilizing algorithm which builds a $k$-clustering of the network. We also certify a quantitative property related to the output of this algorithm. Precisely, we show that the computed $k$-clustering contains at most $\lfloor \frac{n-1}{k+1} \rfloor + 1$ clusterheads, where $n$ is the number of nodes in the network. To obtain these results, we also developed a library which contains general tools related to potential functions and cardinality of sets., Logical Methods in Computer Science ; Volume 13, Issue 4 ; 1860-5974

Published
2016
Full Text
View/download PDF

27. Gradual Stabilization Under $$\tau $$-Dynamics

Author

Stéphane Devismes, Karine Altisen, Anaïs Durand, Franck Petit, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Large-Scale Distributed Systems and Applications (Regal), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011)

Subjects
Property (philosophy), synchronization problems, safe-convergence, Computer science, Quality of service, 020207 software engineering, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, superstabilization, Topology, 01 natural sciences, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], gradual stabilization, 010201 computation theory & mathematics, Feature (computer vision), Dynamics (music), unison, 0202 electrical engineering, electronic engineering, information engineering, Simulation
Abstract

International audience; We introduce the notion of gradually stabilizing algorithm as any self-stabilizing algorithm achieving the following additional feature. If at most τ dynamic steps occur starting from a legitimate configuration, a gradually stabilizing algorithm first quickly recover to a configuration from which a specification offering a minimum quality of service is satisfied. It then gradually converges to specifications offering stronger and stronger safety guarantees until reaching a configuration (1) from which its initial (strong) specification is satisfied again, and (2) where it is ready to achieve gradual convergence again in case of up to $\tau$ new dynamic steps. By definition, a gradually stabilizing algorithm is also self-stabilizing. So, it still recovers within finite time (yet more slowly) after any other finite number of transient faults, including for example more than $\tau$ dynamic steps or other failure patterns such as memory corruptions, for example.We illustrate this new property by considering three variants of a synchronization problem respectively called strong, weak, and partial weak unison. We propose a self-stabilizing algorithm which achieves gradual stabilization in the sense that after one dynamic step from a configuration which is legitimate for the strong unison, it immediately satisfies the specification of partial weak unison, then converges to the specification of weak unison in at most one round, and finally retrieves, after at most (mu+1) D1 + 1 additional rounds, a configuration (1) from which the specification of strong unison is satisfied, and (2) where it is ready to achieve gradual convergence again in case of another dynamic step. D1 is the diameter of the network after the dynamic step, and mu is a parameter satisfying mu >= n + #J, where n is the initial number of processes and #J is an upper bound on the number of processes that join the system during a dynamic step.

Published
2016
Full Text
View/download PDF

28. Leader Election in Rings with Bounded Multiplicity (Short Paper)

Author

Lawrence L. Larmore, Karine Altisen, Stéphane Devismes, Ajoy K. Datta, and Anaïs Durand

Subjects
Discrete mathematics, 020203 distributed computing, Leader election, Short paper, Multiplicity (mathematics), 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Computer Science::Multiagent Systems, Combinatorics, 010201 computation theory & mathematics, Bounded function, 0202 electrical engineering, electronic engineering, information engineering, Mathematics
Abstract

We study leader election in unidirectional rings of homonym processes that have no a priori knowledge on the number of processes. We show that message-terminating leader election is impossible for any class of rings \(\mathcal K_k\) with bounded multiplicity \(k \ge 2\). However, we show that process-terminating leader election is possible in the sub-class \(\mathcal U^* \cap \mathcal K_k\), where \(\mathcal U^*\) is the class of rings which contain a process with a unique label.

Published
2016
Full Text
View/download PDF

29. Concurrency in Snap-Stabilizing Local Resource Allocation

Author

Stéphane Devismes, Karine Altisen, and Anaïs Durand

Subjects
Focus (computing), Computer science, 020204 information systems, Small number, Concurrency, Distributed computing, 0202 electrical engineering, electronic engineering, information engineering, Resource allocation, 020201 artificial intelligence & image processing, 02 engineering and technology, Utilization rate
Abstract

In distributed systems, resource allocation consists in managing fair access of a large number of processes to a typically small number of reusable resources. As soon as the number of available resources is greater than one, the efficiency in concurrent accesses becomes an important issue, as a crucial goal is to maximize the utilization rate of resources. In this paper, we tackle the concurrency issue in resource allocation problems. We first characterize the maximal level of concurrency we can obtain in such problems by proposing the notion of maximal-concurrency. Then, we focus on Local Resource Allocations Problems (LRA). Our results are both negative and positive. On the negative side, we show that it is impossible to obtain maximal-concurrency in LRA without compromising the fairness. On the positive side, we propose a snap-stabilizing LRA algorithm which achieves an high (but not maximal) level of concurrency, called here strong partial maximal-concurrency.

Published
2015
Full Text
View/download PDF

30. [Untitled]

Author

Karine Altisen, Gregor Gössler, and Joseph Sifakis

Subjects
Control and Optimization, Constraint theory, Mathematical model, Computer Networks and Communications, Computer science, Distributed computing, Static timing analysis, Computer Science Applications, Scheduling (computing), Control and Systems Engineering, Composability, restrict, Modeling and Simulation, Electrical and Electronic Engineering, Scheduling theory
Abstract

The controller synthesis paradigm provides a general framework for scheduling real-time applications. Schedulers can be considered as controllers of the applications; they restrict their behavior so that given scheduling requirements are met. We study a modeling methodology based on the controller synthesis paradigm. The methodology allows to get a correctly scheduled system from timed models of its processes in an incremental manner, by application of composability results which simplify schedulability analysis. It consists in restricting successively the system to be scheduled by application of constraints defined from scheduling requirements. The latter are a conjunction of schedulability requirements that express timing properties of the processes and policy requirements about resource management. The presented methodology allows a unified view of scheduling theory and approaches based on timing analysis of models of real-time applications.

Published
2002
Full Text
View/download PDF

31. Stabilisation Instantanée Probabiliste

Author

Karine Altisen, Stéphane Devismes, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011)

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI]
Abstract

International audience; Nous introduisons la stabilisation instantanée probabiliste. Cette propriété nous permet, en particulier, de concevoir des algorithmes distribués pour réseaux anonymes ayant de fortes propriétés de tolérance aux pannes transitoires. Un algorithme instantanément stabilisant probabiliste satisfait la sûreté de sa spécification immédiatement après que les pannes transitoires aient cessé; cependant il n'assure la vivacité de sa spécification que presque sûrement. Nous illustrons cette nouvelle propriété en proposant deux algorithmes instantanément stabilisants probabilistes d'élection avec garantie de service pour réseaux anonymes, ce problème n'ayant pas de solution déterministe.

Published
2014

32. Comparison of Mean Hitting Times for a Degree-Biased Random Walk

Author

Antoine Gerbaud, Pascal Lafourcade, Stéphane Devismes, Karine Altisen, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), SYNCHRONE, Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)

Subjects
Random graph, Discrete mathematics, Heterogeneous random walk in one dimension, Applied Mathematics, 010102 general mathematics, Loop-erased random walk, Hitting time, Simple random sample, Random walk, 01 natural sciences, 010305 fluids & plasmas, Vertex (geometry), Combinatorics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0103 physical sciences, Random regular graph, Discrete Mathematics and Combinatorics, 0101 mathematics, Mathematics, MathematicsofComputing_DISCRETEMATHEMATICS
Abstract

International audience; Consider the random walk on graphs such that, at each step, the next visited vertex is a neighbor of the current vertex, chosen with probability proportional to the inverse of the square root of its degree. On one hand, for every graph with n vertices, the maximal mean hitting time for this degree-biased random walk is asymptotically dominated by n 2. On the other hand, the maximal mean hitting time for the simple random walk is asymptotically dominated by n 3. Yet, in this article, we exhibit for each positive integer n: • A graph of size n with maximal mean hitting time strictly smaller for the simple random walk than for the degree-biased one. • A graph of size n with mean hitting time of a so called root vertex strictly smaller for the simple random walk than for the degree-biased one.

Published
2014
Full Text
View/download PDF

33. On Probabilistic Snap-Stabilization

Author

Karine Altisen and Stéphane Devismes

Subjects
Leader election, Property (philosophy), Theoretical computer science, Computer science, Liveness, Probabilistic logic, Process (computing), Probabilistic analysis of algorithms, Almost surely, Fault (power engineering)
Abstract

In this paper, we introduce probabilistic snap-stabilization. We relax the definition of deterministic snap-stabilization without compromising its safety guarantees. In an unsafe environment, a probabilistically snap-stabilizing algorithm satisfies its safety property immediately after the last fault; whereas its liveness property is only ensured with probability 1. We show that probabilistic snap-stabilization is more expressive than its deterministic counterpart. Indeed, we propose two probabilistic snap-stabilizing algorithms for a problem having no deterministic snap- or self-stabilizing solution: guaranteed service leader election in arbitrary anonymous networks. This problem consists in computing a correct answer to each process that initiates the question "Am I the leader of the network?", i.e., 1 processes always computed the same answer to that question and 2 exactly one process computes the answer true. Our solutions being probabilistically snap-stabilizing, the answers are only delivered within an almost surely finite time; however any delivered answer is correct, regardless the arbitrary initial configuration and provided the question has been properly started.

Published
2014
Full Text
View/download PDF

34. Analysis of Random Walks using Tabu Lists

Author

Karine Altisen, Stéphane Devismes, Antoine Gerbaud, Pascal Lafourcade, VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)

Subjects
Large class, Discrete mathematics, 010102 general mathematics, Hitting time, 0102 computer and information sciences, Random walk, 01 natural sciences, Graph, Tabu list, Combinatorics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], tabu list, 010201 computation theory & mathematics, Bounded function, mean hitting time, 0101 mathematics, Connectivity, Positive probability, Mathematics
Abstract

International audience; A tabu random walk on a graph is a partially self-avoiding random walk which uses a bounded memory to avoid cycles. This memory is called a tabu list and contains vertices already visited by the walker. The size of the tabu list being bounded, the way vertices are inserted and removed from the list, called here an update rule, has an important impact on the performance of the walk, namely the mean hitting time between two given vertices. We define a large class of tabu random walks, characterized by their update rules. We enunciate a necessary and sufficient condition on these update rules that ensures the finiteness of the mean hitting time of their associated walk on every finite and connected graph. According to the memory allocated to the tabu list, we characterize the update rules which yield smallest mean hitting times on a large class of graphs. Finally, we compare the performances of three collections of classical update rules according to the size of their associated tabu list.

Published
2012

35. Causality closure for a new class of curves in real-time calculus

Author

Matthieu Moy, Karine Altisen, SYNCHRONE, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
Discrete mathematics, causality, real-time calculus, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], Closure (topology), 020207 software engineering, 02 engineering and technology, Interval (mathematics), algorithms, Upper and lower bounds, 020202 computer hardware & architecture, Causality (physics), [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], Family of curves, 0202 electrical engineering, electronic engineering, information engineering, Applied mathematics, Finite set, Generator (mathematics), Mathematics, Event (probability theory)
Abstract

International audience; Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by arrival curves which express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. The property of causality on arrival curves essentially characterizes the absence of deadlock in the corresponding generator. A mathematical operation called causality closure transforms arbitrary curves into causal ones. In this paper, we extend the existing theory on causality to the class Upac of infinite curves represented by a finite set of points plus piecewise affine functions, where existing algorithms did not apply. We show how to apply the causality closure on this class of curves, prove that this causal representative is still in the class and give algorithms to compute it. This provides the tightest pair of curves among the curves which accept the same sets of streams.

Published
2011
Full Text
View/download PDF

36. ac2lus: Bringing SMT-Solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre

Author

Matthieu Moy, Karine Altisen, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), FotoVP, ANR-06-SETI-0007,FOTOVP,Outils formels pour le prototypage virtuel des systèmes embarqués(2006), European Project: 215543,EC:FP7:ICT,FP7-ICT-2007-1,COMBEST(2008), and Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Computer science, Programming language, Lustre (programming language), 020207 software engineering, 02 engineering and technology, Abstract interpretation, computer.software_genre, Formal methods, Data structure, Rotation formalisms in three dimensions, Upper and lower bounds, 020202 computer hardware & architecture, [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], Formal specification, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, ComputerSystemsOrganization_SPECIAL-PURPOSEANDAPPLICATION-BASEDSYSTEMS, computer, Data-flow analysis, computer.programming_language
Abstract

We present an approach to connect the Real-Time Calculus (RTC) method to the synchronous data-flow language Lustre, and its associated tool-chain, allowing the use of techniques like SMT-solving and abstract interpretation which were not previously available for use with RTC. The approach is supported by a tool called ac2lus. It allows to model the system to be analyzed as general Lustre programs with inputs specified by arrival curves; the tool can compute output arrival curves or evaluate upper and lower bounds on any variable of the components, like buffer sizes. Compared to existing approaches to connect RTC to other formalisms, we believe that the use of Lustre, a real programming language, and the synchronous hypothesis make the task easier to write models, and we show that it allows a great flexibility of the tool itself, with many variants to fine-tune the performances.

Published
2010
Full Text
View/download PDF

37. Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata

Author

Yanhong Liu, Matthieu Moy, Karine Altisen, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), FotoVP, and ANR-06-SETI-0007,FOTOVP,Outils formels pour le prototypage virtuel des systèmes embarqués(2006)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Speedup, Computer science, Interface (Java), C.4, 02 engineering and technology, granularity, C.3, C.4, F.1.1, lcsh:QA75.5-76.95, 020204 information systems, Component (UML), 0202 electrical engineering, electronic engineering, information engineering, Modular Performance Analysis, State space, Real-Time Calculus, Timed Automata, Uppaal, Computer Science - Performance, lcsh:Mathematics, D.4.7, lcsh:QA1-939, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, 020202 computer hardware & architecture, Automaton, Logic in Computer Science (cs.LO), C.3, Performance (cs.PF), [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], Interfacing, Linear Priced Timed automata, lcsh:Electronic computers. Computer science, Granularity, State (computer science), Algorithm
Abstract

To analyze complex and heterogeneous real-time embedded systems, recent works have proposed interface techniques between real-time calculus (RTC) and timed automata (TA), in order to take advantage of the strengths of each technique for analyzing various components. But the time to analyze a state-based component modeled by TA may be prohibitively high, due to the state space explosion problem. In this paper, we propose a framework of granularity-based interfacing to speed up the analysis of a TA modeled component. First, we abstract fine models to work with event streams at coarse granularity. We perform analysis of the component at multiple coarse granularities and then based on RTC theory, we derive lower and upper bounds on arrival patterns of the fine output streams using the causality closure algorithm. Our framework can help to achieve tradeoffs between precision and analysis time., QAPL 2010

Published
2010
Full Text
View/download PDF

38. Arrival Curves for Real-Time Calculus: the Causality Problem and its Solutions

Author

Karine Altisen, Matthieu Moy, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Combest, Javier Esparza and Rupak Majumdar, ANR-06-SETI-0007,FOTOVP,Outils formels pour le prototypage virtuel des systèmes embarqués(2006), European Project: 215543,EC:FP7:ICT,FP7-ICT-2007-1,COMBEST(2008), and Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, 0209 industrial biotechnology, Arrival Curve, 02 engineering and technology, Interval (mathematics), Upper and lower bounds, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, 020202 computer hardware & architecture, Causality (physics), Causality, [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], 020901 industrial engineering & automation, Family of curves, 0202 electrical engineering, electronic engineering, information engineering, C.3, C.4, Real-Time Calculus, dead-lock, Canonical form, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Algebraic number, Forbidden Regions, Mathematics, Event (probability theory), Generator (mathematics)
Abstract

International audience; The Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by pairs of curves, called arrival curves, that express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. A well-known limitation of RTC is that it cannot model systems with states and recent works studied how to interface RTC curves with state-based models. Doing so, while trying, for example to generate a stream of events that satisfies some given pair of curves, we faced a causality problem: it can be the case that, once having generated a finite prefix of an event stream, the generator deadlocks, since no extension of the prefix can satisfy the curves anymore. When trying to express the property of the curves with state-based models, one may face the same problem. This paper formally defines the problem on arrival curves, and gives algebraic ways to characterize causal pairs of curves, i.e. curves for which the problem cannot occur. Then, we provide algorithms to compute a causal pair of curves equivalent to a given curve, in several models. These algorithms provide a canonical representation for a pair of curves, which is the best pair of curves among the curves equivalent to the ones they take as input.

Published
2010

39. Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis

Author

S. Tripakis, Karine Altisen, Franck Cassez, Institut de Recherche en Communications et en Cybernétique de Nantes (IRCCyN), Mines Nantes (Mines Nantes)-École Centrale de Nantes (ECN)-Ecole Polytechnique de l'Université de Nantes (EPUN), Université de Nantes (UN)-Université de Nantes (UN)-PRES Université Nantes Angers Le Mans (UNAM)-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
0209 industrial biotechnology, Automatic control, Observer (quantum physics), Computer science, Real-time computing, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Observable, Context (language use), 0102 computer and information sciences, 02 engineering and technology, Fault (power engineering), 01 natural sciences, Automaton, Set (abstract data type), 020901 industrial engineering & automation, 010201 computation theory & mathematics, Minification
Abstract

International audience; We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists of synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe.

Published
2007

40. Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems

Author

S. Tripakis, Franck Cassez, and Karine Altisen

Subjects
Observer (quantum physics), Null (SQL), Computer science, Control theory, Real-time computing, Observable, Set (psychology), Fault (power engineering), Fault detection and isolation, Automaton, Event (probability theory)
Abstract

Fault diagnosis consists in synthesizing a diagnoser that observes a given plant through a set of observable events, and identifies faults which are not observable as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe. We define a notion of cost for such dynamic observers and show that (i) the cost of a given dynamic observer can be computed and (ii) an optimal dynamic observer can be synthesized.

Published
2007
Full Text
View/download PDF

41. In this work, we propose two translations: one from extended

Author

Franck Cassez, Karine Altisen, and S. Tripakis

Subjects
Computer engineering, Computer science, Real-time computing, Work (physics), Timed automaton, Fault detection and isolation, Automaton, Digital clock
Abstract

We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification modeled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diagnosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability.

Published
2006
Full Text
View/download PDF

42. Modular Design of Man-Machine Interfaces with Larissa

Author

David Stauch, Karine Altisen, and Florence Maraninchi

Subjects
business.industry, Computer science, Programming language, Interface (Java), Aspect-oriented programming, Modular design, computer.software_genre, Automaton, Set (abstract data type), Component (UML), Component-based software engineering, Artificial intelligence, business, Reactive system, computer
Abstract

The man-machine interface of a small electronic device like a wristwatch is a crucial component, as more and more functions have to be controlled using a small set of buttons. We propose to use Argos, an automaton-based language for reactive systems, and Larissa, its aspect-oriented extension, to show that several interfaces can be obtained from the same set of basic components, assembled in various ways. This is the basis of a quite general component-based development method for man-machine interfaces.

Published
2006
Full Text
View/download PDF

43. Introduction au contrôle des systèmes temps-réel

Author

Patricia Bouyer, Karine Altisen, Franck Cassez, Guillaume Gardey, Thierry Cachat, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'informatique Algorithmique : Fondements et Applications (LIAFA), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche en Communications et en Cybernétique de Nantes (IRCCyN), Mines Nantes (Mines Nantes)-École Centrale de Nantes (ECN)-Ecole Polytechnique de l'Université de Nantes (EPUN), and Université de Nantes (UN)-Université de Nantes (UN)-PRES Université Nantes Angers Le Mans (UNAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[STIC]domain_stic, Computer science, 0102 computer and information sciences, 02 engineering and technology, temporisés, 01 natural sciences, Industrial and Manufacturing Engineering, Computer Science Applications, 010201 computation theory & mathematics, Control and Systems Engineering, Control theory, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Electrical and Electronic Engineering, Reactive system, Game theory, contrôle
Abstract

Ce document est une introduction rapide au domaine du contrôle des sytèmes temporisés

Published
2005

44. Implementation of Timed Automata: An Issue of Semantics or Modeling?

Author

Stavros Tripakis and Karine Altisen

Subjects
Theoretical computer science, Semantics (computer science), Computer science, Property (programming), Timed automaton, Sampling (statistics), Formal methods, Real-time operating system, Execution model, Computer Science::Formal Languages and Automata Theory, Automaton
Abstract

We examine to what extent implementation of timed automata can be achieved using the standard semantics and appropriate modeling, instead of introducing new semantics. We propose an implementation methodology which allows to transform a timed automaton into a program and to check whether the execution of this program on a given platform satisfies a desired property. This is done by modeling the program and the execution platform, respectively, as an untimed automaton and a collection of timed automata. We also study the problem of property preservation, in particular when moving to a “better” execution platform. We show that some subtleties arise regarding the definition of “better”, in particular for digital clocks. The fundamental issue is that faster clocks result in better “sampling” and therefore can introduce more behaviors.

Published
2005
Full Text
View/download PDF

45. Implémentabilité des automates temporisés

Author

Nicolas Markey, Stavros Tripakis, Karine Altisen, Pierre-Alain Reynier, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'informatique Fondamentale de Marseille - UMR 6166 (LIF), Université de la Méditerranée - Aix-Marseille 2-Université de Provence - Aix-Marseille 1-Centre National de la Recherche Scientifique (CNRS), Alla, Hassane and Rutten, Éric, Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Markey, Nicolas, and Alla, Hassane and Rutten, Éric

Subjects
Model checking, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, Knowledge representation and reasoning, Semantics (computer science), Computer science, Timed automaton, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, Nonlinear Sciences::Cellular Automata and Lattice Gases, 01 natural sciences, Industrial and Manufacturing Engineering, Computer Science Applications, Automaton, 010201 computation theory & mathematics, Control and Systems Engineering, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Electrical and Electronic Engineering, Reactive system, Computer Science::Formal Languages and Automata Theory
Abstract

International audience; In this paper, we present the problem of the implementability of timed automata. The theoretical semantics of timed automata can not be exactly implemented in practice, because computers are digital and more or less precise; the properties verified on a timed automaton are not necessarily preserved when implementing it. We deal with two approaches: the first one is based on the modeling of the execution platform and the second studies an enlarged semantics for timed automata that takes the imprecision into account.

Published
2005

46. Using Controller-Synthesis Techniques to Build Property-Enforcing Layers

Author

Eric Rutten, Florence Maraninchi, Karine Altisen, and Aurélie Clodic

Subjects
Set (abstract data type), Mealy machine, Theoretical computer science, Control theory, Computer science, Component (UML), Product (mathematics), Distributed computing, Temporal logic, Constraint (mathematics), Automaton
Abstract

In complex systems, like robot plants, applications are built on top of a set of components, or devices. Each of them has particular individual constraints, and there are also logical constraints on their interactions, related to e.g., mechanical characteristics or access to shared resources. Managing these constraints may be separated from the application, and performed by an intermediate layer. We show how to build such property-enforcing layers, in a mixed imperative/ declarative style: 1) the constraints intrinsic to one component are modeled by an automaton; the product of these automata is a first approximation of the set of constraints that should be respected; 2) the constraints that involve several components are expressed as temporal logic properties of this product; 3) we use general controller synthesis techniques and tools in order to combine the set of communicating parallel automata with the global constraint.

Published
2003
Full Text
View/download PDF

47. On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems

Author

Stavros Tripakis and Karine Altisen

Subjects
Bisimulation, Reachability, Control theory, Computer science, Computer Science::Logic in Computer Science, Timed automaton, State space, Context (language use), Algorithm, Quotient graph, Formal verification, Computer Science::Formal Languages and Automata Theory, Automaton
Abstract

We present novel techniques for efficient controller synthesis for untimed and timed systems with respect to invariance and reachability properties. In the untimed case, we give algorithms for controller synthesis in the context of finite graphs with controllable and uncontrollable edges, distinguishing between the actions of the system and its environment, respectively. The algorithms are on-the-fly, since they return a controller as soon as one is found, which avoids the generation of the whole state space. In the timed case, we use the model of timed automata extended with controllable and uncontrollable discrete transitions. Our controller-synthesis method here is only half on-the-fly, since it relies on the a-priori generation of a finite model (graph) of the timed automaton, as quotient of the time-abstracting bisimulation. The quotient graph is essentially an untimed graph, upon which we can apply the untimed on-the-fly algorithms to compute a timed controller.

Published
1999
Full Text
View/download PDF

48. Concurrency in Snap-Stabilizing Local Resource Allocation

Author

Stéphane Devismes, Anaïs Durand, Karine Altisen, SYNCHRONE, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011)

Subjects
Critical section, Theoretical computer science, Computer Networks and Communications, Computer science, Concurrency, Distributed computing, Distributed concurrency control, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Theoretical Computer Science, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], 010201 computation theory & mathematics, Artificial Intelligence, Hardware and Architecture, Distributed algorithm, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Resource allocation, Mutual exclusion, Optimistic concurrency control, Software
Abstract

In distributed systems, resource allocation consists in managing fair access of a large number of processes to a typically small number of reusable resources. As soon as the number of available resources is greater than one, the efficiency in concurrent accesses becomes an important issue, as a crucial goal is to maximize the utilization rate of resources. In this paper, we tackle the concurrency issue in resource allocation problems. We first characterize the maximal level of concurrency we can obtain in such problems by proposing the notion of maximal concurrency. Then, we focus on Local Resource Allocation problems (LRA). Our results are both negative and positive. On the negative side, we show that there is a wide class of instances of LRA for which it is impossible to obtain maximal concurrency without compromising the fairness. On the positive side, we propose a snap-stabilizing LRA algorithm which achieves a high (but not maximal) level of concurrency, called here strong concurrency. We define several notions of concurrency, including maximal concurrency which is the maximal level of concurrency achievable in a resource allocation problem.We show that maximal concurrency cannot always be achieved in Local Resource Allocation (LRA) problems.We propose a snap-stabilizing LRA algorithm achieving a high (but not maximal) level of concurrency.

49. Routage par marche aléatoire à listes tabous

Author

Karine Altisen, Stéphane Devismes, pascal lafourcade, Clément Ponsonnet, VERIMAG (VERIMAG - IMAG), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], routage, marche aléatoire, Réseaux de capteurs sans fil, liste tabou
Abstract

International audience; Nous proposons d'améliorer les marches aléatoires en utilisant des listes tabous. Notre objectif est de réduire le nombre de sauts pour atteindre un noeud particulier du réseau sans compromettre les autres avantages des marches aléatoires. Nos solutions permettent ainsi de résoudre efficacement le routage dans les réseaux de capteurs sans fil.

50. Self-stabilizing Systems in Spite of High Dynamics

Author

Colette Johnen, Stéphane Devismes, Karine Altisen, Franck Petit, Anaïs Durand, VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, This study has been partially supported by the ANR project Estate (ANR-16-CE25-0009), LaBRI, CNRS UMR 5800, ANR-16-CE25-0009,ESTATE,Enhancing Safety and self-sTAbilization in Time-varying distributed Environments(2016), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Modélisation, Information et Systèmes - UR UPJV 4290 (MIS), Université de Picardie Jules Verne (UPJV), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), LIP6, ANR-22-CE25-0008,SKYDATA,Un nouveau paradigme de donnée: Les données autononomes et intelligentes(2022), ANR-16-CE25-0009,ESTATE,Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps(2016), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne), and Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Leader election, Class (set theory), General Computer Science, Computer science, Self-stabilization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, 2012 ACM Subject Classification : Theory of computation→Distributed algorithms, Theoretical Computer Science, [INFO.INFO-MC]Computer Science [cs]/Mobile Computing, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Evolving graphs, ComputingMilieux_MISCELLANEOUS, Discrete mathematics, time-varying graphs, Message passing, Process (computing), 020206 networking & telecommunications, Tiime-varying graphs, Identifier, 010201 computation theory & mathematics, Bounded function, Spite, Speculation, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
Abstract

International audience; We initiate research on self-stabilization in highly dynamic identified message-passing systems where dynamics is modeled using time-varying graphs (TVGs). More precisely, we address the self-stabilizing leader election problem in three wide classes of TVGs: the class TCB(Δ) of TVGs with temporal diameter bounded by Δ, the class TCQ(Δ) of TVGs with temporal diameter quasi-bounded by Δ, and the class TCR of TVGs with recurrent connectivity only, where TCB(Δ)⊆TCQ(Δ)⊆TCR. We first study conditions under which our problem can be solved. We introduce the notion of size-ambiguity to show that the assumption on the knowledge of the number n of processes is central. Our results reveal that, despite the existence of unique process identifiers, any deterministic self-stabilizing leader election algorithm working on the class TCQ(Δ) or TCR cannot be size-ambiguous, justifying why our solutions for those classes assume the exact knowledge of n. We then present three self-stabilizing leader election algorithms for Classes TCB(Δ), TCQ(Δ), and TCR, respectively. Our algorithm for TCB(Δ) stabilizes in at most 3Δ rounds. However, we show that stabilization time cannot be bounded for the leader election problem in TCQ(Δ) and TCR. Nevertheless, we circumvent this issue by showing that our solutions are speculative in the sense that their stabilization time in TCB(Δ) (⊆TCQ(Δ)⊆TCR) is O(Δ) rounds.

Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results