Timed Automata Robustness Analysis via Model Checking

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BENDÍK Jaroslav SENCAN Ahmet GOL Ebru Aydin ČERNÁ Ivana

Rok publikování 2022
Druh Článek v odborném periodiku
Časopis / Zdroj Logical Methods in Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://lmcs.episciences.org/9864
Doi http://dx.doi.org/10.46298/lmcs-18(3:12)2022
Klíčová slova Timed Automata; Design; Reachability; Safety
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.