Robust synthesis for real-time systems
Robust synthesis for real-time systems
复制标题
DOI：
10.1016/j.tcs.2013.08.015
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
K. Larsen;Axel Legay;Louis-Marie Traonouez;A. Wąsowski
中科院分区：
文献类型：
--
作者：
K. Larsen;Axel Legay;Louis-Marie Traonouez;A. Wąsowski
实时系统的规范理论允许推理接口及其实现模型，使用一组操作符，包括满意度，细化，逻辑和并行组合。为了使这些理论适用于从抽象规范到实现的整个设计过程，我们需要考虑在物理系统上有效实现理论规范的可能性，尽管它们的精度有限。在文献中，这个实现问题已被链接到鲁棒性问题，分析的后果，引入小扰动正式models.We解决这个问题的鲁棒性实现定时规范理论。我们首先考虑一个固定的扰动和研究的鲁棒性的时间规格方面的运营商的理论。为此，我们在定时游戏中合成强大的策略。最后，我们考虑参数鲁棒性问题，并提出了一个反例细化启发式计算安全扰动值。
Specification theories for real-time systems allow reasoning about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to reason about the possibility to effectively implement the theoretical specifications on physical systems, despite their limited precision. In the literature, this implementation problem has been linked to the robustness problem that analyzes the consequences of introducing small perturbations into formal models.We address this problem of robust implementations in timed specification theories. We first consider a fixed perturbation and study the robustness of timed specifications with respect to the operators of the theory. To this end we synthesize robust strategies in timed games. Finally, we consider the parametric robustness problem and propose a counter-example refinement heuristic for computing safe perturbation values.