ATAC: A Tool for Automating Timed Automata Construction
This work provides a tool for system designers to more easily create and verify timed automata models, but the approach is incremental as it relies on a predefined structured language and does not demonstrate quantitative improvements over manual methods.
The paper introduces ATAC, a tool that automates the construction of timed automata (TA) models from structured natural language descriptions and generates temporal logic queries from specifications, enabling import into UPPAAL for verification. The goal is to accelerate the design phase for real-time systems by reducing errors in initial model construction.
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.