English

ATAC: A Tool for Automating Timed Automata Construction

Formal Languages and Automata Theory 2020-07-03 v2 Systems and Control

Abstract

In this paper, we focus on the design and verification of timed automata (TA). We introduce a new method for assisting construction and verification of TA models along with a tool implementing the proposed method, i.e., ATAC: Automated Timed Automata Construction. Our method provides two main functionalities, i.e., construction of TA models from descriptions and generation of temporal logic queries from specifications. Both description and specification sentences shall follow our well-defined structured natural language definition. TA models constructed from descriptions and temporal logic queries generated from specifications can be imported to UPPAAL, a verification tool for TA models. The goal is to accelerate the design phase for real-time systems by assisting the construction and verification of a formal model. We believe ATAC can be useful especially during the initial phases of the design process and help designers to avoid erroneous models.

Keywords

Cite

@article{arxiv.1905.08169,
  title  = {ATAC: A Tool for Automating Timed Automata Construction},
  author = {Beyazit Yalcinkaya and Ebru Aydin Gol},
  journal= {arXiv preprint arXiv:1905.08169},
  year   = {2020}
}

Comments

10 pages, 1 figure, tool paper

R2 v1 2026-06-23T09:13:37.168Z