A Parametric Counterexample Refinement Approach for Robust Timed Specifications

Louis-Marie Traonouez
(Aalborg University)

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.

Invited Paper in Sebastian Bauer and Jean-Baptiste Raclet: Proceedings Fourth Workshop on Foundations of Interface Technologies (FIT 2012), Tallinn, Estonia, 25th March 2012, Electronic Proceedings in Theoretical Computer Science 87, pp. 17–33.
Published: 15th July 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.87.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org