Timed automata (TA) have been widely adopted as a suitable formalism to model time-critical systems. Furthermore, contemporary model-checking tools allow the designer to check whether a TA complies with a system specification. However, the exact timing constants are often uncertain during the design phase. Consequently, the designer is often able to build a TA with a correct structure, however, the timing constants need to be tuned to satisfy the specification. Moreover, even if the TA initially satisfies the specification, it can be the case that just a slight perturbation during the implementation causes a violation of the specification. Unfortunately, model-checking tools are usually not able to provide any reasonable guidance on how to fix the model in such situations. In this paper, we propose several concepts and techniques to cope with the above mentioned design phase issues when dealing with reachability and safety specifications.

翻译：时间自动数据(TA)被广泛采用,作为模拟时间临界系统的适当形式,此外,现代模型检查工具允许设计者检查技术助理是否符合系统规格,但设计阶段的精确时间常数往往不确定,因此设计者往往能够建立一个结构正确的技术助理,但时间常数需要调整才能满足规格。此外,即使技术助理人员最初满足规格要求,执行过程中的轻微扰动可能违反规格。不幸的是,模型检查工具通常无法提供合理指导,说明如何在此种情况下修复模型。在本文件中,我们提出了在处理可达性和安全规格时应对上述设计阶段问题的若干概念和技术。