2012/07/14 by Louis‐Marie Traonouez, Louis-Marie Traonouez · 10 citations
Computer Science · Mathematics · #Algorithm #Automaton #Computer science #Counterexample #Discrete mathematics #Formal Methods in Verification #Mathematics #Parametric statistics #Perturbation (astronomy) #Programming language #Robustness (evolution) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #Theoretical computer science #cs.FL #cs.SE
paper · pdf · doi:10.4204/eptcs.87.3
published in Electronic Proceedings in Theoretical Computer Science 87, 17-33 (Open Publishing Association) · In Proceedings FIT 2012, arXiv:1207.3485
openalex publication_date 2012/07/14 · arxiv created 2012/07/18 · arxiv updated 2012/07/19 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
Robustness analyzes the impact of small perturbations in the semantics of a model. This allows to model hardware imprecision and therefore it has been applied to determine implementability of timed automata. In a recent paper, we extend this problem to a specification theory for real-timed systems based on timed input/output automata, that are interpreted as two-player games. We propose a construction that allows to synthesize an implementation of a specification that is robust under a given timed perturbation, and we study the impact of these perturbations when composing different specifications. To complete this work we present a technique that evaluates the greatest admissible perturbation. It consists in an iterative process that extracts a spoiling strategy when a game is lost, and through a parametric analysis refines the admissible values for the perturbation. We demonstrate this approach with a prototype implementation.