Timed Automata Robustness Analysis via Model Checking

J 2022

Timed Automata Robustness Analysis via Model Checking

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

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

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í

Odkazy

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ěněno: 28. 3. 2023 11:46, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 VaV

Název: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur

Citovat

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.

@article{1876637,
   author = {Bendík, Jaroslav and Sencan, Ahmet and Gol, Ebru Aydin and Černá, Ivana},
   article_number = {3},
   doi = {http://dx.doi.org/10.46298/lmcs-18(3:12)2022},
   keywords = {Timed Automata; Design; Reachability; Safety},
   language = {eng},
   issn = {1860-5974},
   journal = {Logical Methods in Computer Science},
   title = {Timed Automata Robustness Analysis via Model Checking},
   url = {https://lmcs.episciences.org/9864},
   volume = {18},
   year = {2022}
}

TY  - JOUR
ID  - 1876637
AU  - Bendík, Jaroslav - Sencan, Ahmet - Gol, Ebru Aydin - Černá, Ivana
PY  - 2022
TI  - Timed Automata Robustness Analysis via Model Checking
JF  - Logical Methods in Computer Science
VL  - 18
IS  - 3
SP  - 1-32
EP  - 1-32
SN  - 18605974
KW  - Timed Automata
KW  - Design
KW  - Reachability
KW  - Safety
UR  - https://lmcs.episciences.org/9864
N2  - 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.
ER  -

BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL a Ivana ČERNÁ. Timed Automata Robustness Analysis via Model Checking. \textit{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.

Podrobný výpis o publikaci