文章基本信息
- 标题：A Parametric Counterexample Refinement Approach for Robust Timed Specifications
- 本地全文：下载
- 作者：Louis-Marie Traonouez
- 期刊名称：Electronic Proceedings in Theoretical Computer Science
- 电子版ISSN：2075-2180
- 出版年度：2012
- 卷号：87
- 页码：17-33
- DOI：10.4204/EPTCS.87.3
- 出版社：Open Publishing Association
- 摘要：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.
