BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL a Ivana ČERNÁ. Timed Automata Robustness Analysis via Model Checking. Logical Methods in Computer Science. 2022, roč. 18, č. 3, s. 1-32. ISSN 1860-5974. Dostupné z: https://dx.doi.org/10.46298/lmcs-18(3:12)2022.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Timed Automata Robustness Analysis via Model Checking
Autoři BENDÍK, Jaroslav (203 Česká republika), Ahmet SENCAN, Ebru Aydin GOL a Ivana ČERNÁ (203 Česká republika, garant, domácí).
Vydání Logical Methods in Computer Science, 2022, 1860-5974.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
WWW URL URL
Impakt faktor Impact factor: 0.600
Kód RIV RIV/00216224:14330/22:00126329
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.46298/lmcs-18(3:12)2022
UT WoS 000835341300002
Klíčová slova anglicky Timed Automata; Design; Reachability; Safety
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 3. 2023 11:46.
Anotace
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.
Návaznosti
EF16_019/0000822, projekt VaVNázev: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur
VytisknoutZobrazeno: 19. 9. 2024 16:56