Timed Automata Robustness Analysis via Model Checking

Timed automata (TA) have been widely adopted as a suitable formalism to modeltime-critical systems. Furthermore, contemporary model-checking tools allow thedesigner 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 correctstructure, however, the timing constants need to be tuned to satisfy thespecification. Moreover, even if the TA initially satisfies the specification,it can be the case that just a slight perturbation during the implementationcauses a violation of the specification. Unfortunately, model-checking toolsare usually not able to provide any reasonable guidance on how to fix the modelin such situations. In this paper, we propose several concepts and techniquesto cope with the above mentioned design phase issues when dealing withreachability and safety specifications