# ATAC: A Tool for Automating Timed Automata Construction

## TL;DR

This paper presents ATAC, a tool that automates the construction and verification of timed automata models from structured natural language descriptions, aiming to streamline the design process of real-time systems.

## Contribution

It introduces a novel method and tool for automatically generating timed automata models and temporal logic queries from natural language, facilitating early-stage design and verification.

## Key findings

- Enables automatic construction of TA models from descriptions
- Supports generation of temporal logic queries from specifications
- Integrates with UPPAAL for verification

## 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.