Jaroslav Bendík ; Ahmet Sencan ; Ebru Aydin Gol ; Ivana Černá - Timed Automata Robustness Analysis via Model Checking

lmcs:8375 - Logical Methods in Computer Science, July 29, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:12)2022
Timed Automata Robustness Analysis via Model CheckingArticle

Authors: Jaroslav Bendík ; Ahmet Sencan ; Ebru Aydin Gol ; Ivana Černá ORCID

    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.


    Volume: Volume 18, Issue 3
    Published on: July 29, 2022
    Accepted on: May 12, 2022
    Submitted on: August 19, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • imPACT – Privacy, Accountability, Compliance, and Trust in Tomorrow’s Internet; Funder: European Commission; Code: 610150
    • Automating Timed Automata Design; Funder: European Commission; Code: 798482

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1581 times.
    This article's PDF has been downloaded 559 times.