BENDÍK, Jaroslav, Ahmet SENCAN, Ebru Aydin GOL and Ivana ČERNÁ. Timed Automata Robustness Analysis via Model Checking. Logical Methods in Computer Science. 2022, vol. 18, No 3, p. 1-32. ISSN 1860-5974. Available from: https://dx.doi.org/10.46298/lmcs-18(3:12)2022.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Timed Automata Robustness Analysis via Model Checking
Authors BENDÍK, Jaroslav (203 Czech Republic), Ahmet SENCAN, Ebru Aydin GOL and Ivana ČERNÁ (203 Czech Republic, guarantor, belonging to the institution).
Edition Logical Methods in Computer Science, 2022, 1860-5974.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
WWW URL URL
Impact factor Impact factor: 0.600
RIV identification code RIV/00216224:14330/22:00126329
Organization unit Faculty of Informatics
Doi http://dx.doi.org/10.46298/lmcs-18(3:12)2022
UT WoS 000835341300002
Keywords in English Timed Automata; Design; Reachability; Safety
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/3/2023 11:46.
Abstract
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.
Links
EF16_019/0000822, research and development projectName: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur
PrintDisplayed: 21/7/2024 11:34