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.

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.

Equations

$${\varphi }_{TA}::=$$

$${\varphi }_{init}::=$$

$$\mid$$

$${\varphi }_{sys}::=$$

$${\varphi }_{invrt}::=$$

$${\varphi }_{tran}::=$$

$$\mid$$

$${\varphi }_{locs}::=$$

$${\varphi }_{sc}::=$$

$${\varphi }_{tc}::=$$

$${\varphi }_{ic}::=$$

$${\varphi }_{tcons}::=$$

$$\mid$$

$${\varphi }_{icons}::=$$

$${\varphi }_{eq}::=$$

$${\varphi }_{el}::=$$

$${\varphi }_{go}::=$$

$${\varphi }_{spec}::=$$

$$\mid$$

$${\varphi }_{pf}::=$$

$$\mid$$

$${\varphi }_{sf}::=$$

$${\varphi }_{atom}::=$$

$$\mid$$

$${\varphi }_{op}::=$$

Full text

1 Introduction

Cyber-physical systems (CPS) are everywhere and they are getting increasingly more attention from the research community as well as the industry with the advancements in the digital transformation and increase in the adaptation of intelligent systems. As their application areas increase, models representing CPS are getting more complex and sophisticated. Systems with timing requirements, i.e., real-time systems (RTS), are an essential part of CPS. Timed automata (TA) [1, 2, 3], a widely-used and well-known RTS formalism, is used for modeling, designing, and verifying CPS. From railroad crossing systems [4, 5] to cardiac pacemakers [6] to scheduling of real-time systems [7, 8, 9], TA are used to model and analyze numerous systems. Algorithms for verifying TA against formal specifications such as temporal logics exist and implemented in various tools including UPPAAL [10], a tool for modeling, designing, and verifying TA models.

As CPS get more complicated, designing reliable TA models is getting tedious and error-prone. Since most of the RTS are safety-critical, errors in the design of TA models are not tolerable. However, since there is no automated way of TA design and no well-defined design procedure to follow, designing TA models inherently requires human creativity and knowledge, which is an unavoidable source of error and considerably dangerous for safety-critical systems.

This paper

We introduce novel methods to assist TA design. We generate TA models and temporal logic formulas from specifications and system descriptions given in structured natural language in an automated way. We restrict description and specification sentences to a limited set of English sentences to simplify the design descriptions. Given a description sentence, any implied timing, synchronization, and transition information about the system are extracted, then a TA model following these descriptions is constructed. For the specification sentences, specifications are mapped to formulas in the UPPAAL’s query language, a subset of Timed Computation Tree Logic (TCTL). If there is a specific timing behavior implied by the given sentence, the necessary clocks are placed on the model so that the corresponding formula can be verified. That is, a non-trivial mapping is performed from input sentences to TA models and temporal logic queries by taking care of low-level design choices such as clock allocations, synchronization of TA models, and generation of temporal logic formulas. The goal is to assist development of TA models, not to fully automate the whole design process. Although, the developed methods allow users to define complete TA models, we foresee that for a complex model, description sentences would be too long and it would not be simpler than manually designing the model. For this reason, we believe the proposed methods would be useful to construct a skeleton for the complex model together with the placement of necessary clocks for the verification of timing properties, and then the user can take over to add the task-specific components of the model. The developed methods are implemented as a Python program named ATAC (Automated Timed Automata Construction). Given the system descriptions and specifications, ATAC outputs an XML file and a query file which can be imported to UPPAAL.

Related Work

To the best of out knowledge, the proposed method is the first attempt to automate TA construction at this level. Although, there has been some work on different aspects of TA generation such as parameter synthesis [11] and controller synthesis [12], no prior work has been focused on the automation of TA design. In [13], the authors present a theoretic approach to the problem of automatic synthesis of real-time systems. In their solution, from a given set of timed models and a real-time logical specification, they check the existence of a real-time model which can yield a TA network satisfying given specification. In LTLMop Project [14], a set of sentences are mapped to Linear Temporal Logic (LTL) specifications for robot control by defining a formal grammar. In [15], IMITATOR is presented which is a tool for parametric verification and robustness analysis of parametric timed automata. In [16], a transformation method from programmable logic controllers represented with functional block diagrams to a TA model has been introduced. However, no work has been done on assisting TA design at the level of structured natural language.

The paper is outlined as follows. Sec. 2 presents basic definitions of TA and UPPAAL. Sec. 3 and Sec. 4 present details of the TA construction and specification generation, respectively. Sec. 5 reveals details of ATAC . Sec. 6 elaborates a case study, and Sec. 7 concludes the paper.

2 Timed Automata

A timed automaton (TA) [1, 3, 17] is a finite-state machine extended with a finite set of real-valued clocks progressing monotonically and measuring the time spent after their latest resets. $\Phi(C)$ is a set of clock constraints over a set of clocks $C$. A clock constraint $\phi\in\Phi(C)$ is given by the grammar: $\phi::=x\leq c\mid x\geq c\mid x<c\mid x>c\mid\phi\land\phi$, where $x\in C$ and $c\in\mathbb{Q}$.

Definition 1 (Timed Automata)

A timed automaton $\mathscr{A}=(L,l_{0},\Sigma,C,I,T)$ is a tuple, where (i) $L$ is a finite set of locations, (ii) $l_{0}\in L$ is an initial location, (iii) $\Sigma$ is a finite set of labels, (iv) $C$ is a finite set of clocks, (v) $I$ is a mapping from $L$ to $\Phi(C)$, and (vi) $T\subseteq L\times\Sigma\times 2^{C}\times\Phi(C)\times L$ is a set of transitions. $t=(l_{s},\alpha,\lambda,\phi,l_{t})\in T$ is a transition from $l_{s}$ to $l_{t}$ on symbol $\alpha$. $\lambda$ is a set of clocks reset to zero on $t$ and $\phi$ is a clock constraint tested for enabling $t$.

UPPAAL [10, 18], is a tool for modeling, designing, simulating, and verifying TA. UPPAAL extends the TA formalism to provide wider implementation opportunities for RTS. One such extension is the synchronization channels that can be added to transitions to synchronize two TA, i.e., the synchronized TAs have to take the transition at the same time. The developed methods support the synchronization channels as it is fundamental to model network of RTS. However, other extensions are omitted to avoid complicated descriptions.

3 Timed Automata Construction

In this section, we define proposed approach to generate a TA model from high level descriptions of a RTS. First, we define a formal grammar for the system description sentences. For a set of sentences following this grammar, we construct a TA by allocating locations, transitions, clocks, and synchronization channels by inferring details of the model in an automated way. Eqn. (1) defines main grammar rules for the TA construction. Notice that, in this definition, A indicates name of a TA model, L indicates name of a location, S indicates name of a synchronization channel, italic font indicates strings appearing in the rules, and $\epsilon$ is the empty string. A set of sentences for describing a TA model should follow the rule $\phi_{TA}$.

To define a TA (1a), first, an initialization sentence following $\phi_{init}$ should be given. It declares name of the model and its locations. If the model contains a single location (1b), otherwise (1c) should be used. System sentences (1d) follow the initialization sentence. These sentences can refer to either invariance properties (1e) or transitions (1f-1k) of the model.

[TABLE]

Grammar defines six distinct transition types: Simple transition (1f) defines a transition from a set of locations to a set of locations. Synchronization transition (1g) defines a simple transition sending a synchronization signal. Synchronization conditional simple transition (1h) defines a simple transition which can only be taken if a synchronization signal is received. Time conditional simple transition (1i) defines a simple transition which can only be taken if a condition on clocks is satisfied. Time conditional synchronization transition (1j) defines a synchronization transition which can only be taken if a condition on clocks is satisfied. Synchronization-time conditional simple transition (1k) defines a simple transition which can only be taken if a synchronization signal is received and a condition on clocks is satisfied.

Eqn. (2) presents helper grammar rules. Locations (2a) defines a set of locations in the model; synchronization condition (2b) indicates a synchronization condition; transition condition (2c) describes a time condition implicitly referring existence of some clocks without giving any low-level details; invariant condition (2d) is similar to a transition condition as it also defines a time condition but for a location invariant; time constraint (2e) describes a timing constraint by relational operators; invariant constraint (2f) defines a timing constraint by using only more than and more than or equal to relational operators; equality (2g) indicates either existence or nonexistence of the equality case for relational operators; entering or leaving (2h) indicates if the transition under consideration is either entering or leaving mentioned location in the sentence; and finally, go (2i) indicates transitions from a set of locations to a set locations.

Note that clocks are not explicitly defined in the grammar. For transition conditions and invariant conditions, the clock allocation, reset placement, and constraint generation are performed in an automated way. In particular, for each transition and invariant condition appearing in the description, a new clock is created. If the sentence refers to a condition depending on entering a location, then this new clock is reset on each transition that ends in the given location. If the sentence refers to a condition depending on leaving a location, then the clock is reset on each transition that leaves the given location. This entering/leaving information for resetting clocks is inferred from $\phi_{el}$ rule in the grammar. To generate conditions of a clock, we extract the information given by $\phi_{tc}$ and $\phi_{ic}$.

[TABLE]

It is ensured that ordering of the description sentences is not significant, i.e., a given set of sentences following the description grammar is mapped to a unique TA for any ordering. Once all the description sentences are analyzed for a TA, the clock reduction algorithm from [19] is applied to reduce the number of clocks. As each timing constraint is, initially, encoded with a separate clock, the clock reduction step significantly reduces the number of clocks, which is essential to reduce the verification time and improve maintainability of the model.

4 Specification Generation

In this section, we define the structure for the specification sentences, the mapping to the TCTL formulas and the corresponding query in the UPPAAL’s query language. In addition to formula generation, for a specification with a timing condition, we place a new clock on the model and generate the formula with respect to this new clock. That is, the user does not specify anything regarding a new clock and its value (similar to the description grammar). Only a high-level specification is given by the user and the necessary clock placement is performed automatically for the verification of the inferred formula. We define the structured natural language sentences for generating queries with a formal grammar which entirely covers UPPAAL’s query language. Notice that, the same convention as in the specification grammar and some of the helper rules are used. A specification sentence should follow the rule $\phi_{spec}$ in Eqn. 3.

Four distinct specification types are defined by the grammar: General (3a) defines the general format of UPPAAL’s query language which is a subset of TCTL. Since UPPAAL does not allow nested path formulas, the general query format can be realized by a path formula ($\phi_{pf}$) followed by a state formula ($\phi_{sf}$), which is further explained below. Deadlock (3b) indicates the special case of UPPAAL’s query language for checking the existence of a deadlock. This rule is mapped to the following TCTL formula: \say$A\square\neg deadlock$ which is written as \sayA[] not deadlock in UPPAAL. Leads to (3c) is again a special case of UPPAAL’s query language. A sentence following this rule basically says that a state formula leads to another state formula. Suppose a sentence following (3c) is given as “$\psi_{1}$ leads to $\psi_{2}$”, then this sentence is mapped to the following TCTL formula: $A\square(\psi_{1}\implies A\diamond\psi_{2})$ which is written as \say$\psi_{1}$ --> $\psi_{2}$ in UPPAAL. Shorthand (3d) is a shorthand rule that we introduced for convenience. It indicates that a given location shall always be visited within a specific amount of time. Suppose a sentence is given following this rule and it belongs to a TA named Template, name of the inferred location is Location, and the amount of time specified is $4$, then the tool maps it to the following TCTL formula: \say$A\square\ \neg Template.Location\ \lor\ x\leq 4$ which is written as \sayA[] not Template.Location or x <= 4 in UPPAAL. Notice that x is a clock variable that is automatically created and it is reset to zero in every transition leaving given location.

[TABLE]

Path formulas (3e) are mapped to TCTL path formulas as follows: shall always is mapped to $A\square$, shall eventually is mapped to $A\diamond$, might always is mapped to $E\square$, and shall eventually is mapped to $E\diamond$. State formulas (3f) can either be an atomic proposition or some atomic propositions connected by conjunction, disjunction, and implication. Atomic propositions (3g) can infer to either a time condition or visiting a location of the model.

For each time condition, a unique clock is generated. The clock reduction process is not applied to these clocks. They are only reset to zero on necessary transitions of the model and only checked in the generated queries. This functionality allows users to avoid manual clock allocations for the verification of specifications.

5 Implementation of ATAC

TA and formula construction methods presented in this paper are implemented as a Python program called ATAC  [20]. The user can give multiple TA descriptions ($\phi_{TA}$ (1)) to construct a network of TA. Descriptions of these TA can intersect, i.e., TA descriptions does not need to be sequential. ATAC handles allocation of locations, transitions, clocks, and synchronization channels automatically as described in Sec. 3 and Sec. 4. The tool also implements the clock reduction algorithm from [19] that reduces the number of clocks via clock renaming. As described in Sec. 3, initially a new clock is generated for each sentence with a time condition, which results in a large number of clocks. Then, the reduction is performed to reduce the number of clocks. After TA construction, clock reduction, and specification mapping, the resulting TA is mapped to an XML file and its specifications are mapped to a query file. Both of these files can be imported to UPPAAL.

6 A Case Study: Train-Gate TA

In this section, we present a case study to illustrate the proposed methods and the intended usage of ATAC . We picked a well-know example which is also provided in the installation package of UPPAAL as a demo example, i.e., Train-Gate model (Fig. 1). This model consists of two TA models: a train and a gate. A certain number of the train model can be instantiated and each instance of the train TA is given an identification number ($id$). There is a single instantiation for the gate TA controlling which train to pass the gate and which ones to wait. The communication between the gate and trains is performed by an array of synchronization channels. The channel array is indexed by train ids. In addition to the channel array, the model uses other extensions implemented in UPPAAL such as nondeterministic selection of integers, C-like programming structures, and committed locations.

6.1 Description of Train TA

Below, we list description sentences to construct the model given in Fig. 1-(a). Notice that with the clock reduction algorithm, our tool automatically reduces the number of clocks to one for multiple timing requirements on the model. Fig. 1-(b) presents the TA model obtained after manual modification of the automatically constructed model. To obtain the final model, only some C-like programming structures and channel indexes are added to the model manually.

• •

Train can be Safe Appr Cross Stop Start and it is initially Safe.

• •

Train can send Appr and go from Safe to Appr.

• •

If the time spent after entering Appr is more than or equal to 10, then Train can go from Appr to Cross.

• •

If Stop is received and the time spent after entering Appr is less than or equal to 10, then Train can go from Appr to Stop.

• •

If Go is received, then Train can go from Stop to Start.

• •

If the time spent after entering Start is more than or equal to 7, then Train can go from Start to Cross.

• •

If the time spent after entering Cross is more than or equal to 3, then Train can send Leave and go from Cross to Safe.

• •

For Train, the time spent in Appr cannot be more than 20.

• •

For Train, the time spent in Start cannot be more than 15.

• •

For Train, the time spent in Cross cannot be more than 5.

6.2 Description of Gate TA

Below, we list description sentences for Gate TA given in Fig. 1-(c). Four sentences are needed for this model. Fig. 1-(d) presents the TA model obtained after manual modification of the automatically constructed model. To obtain the final model, only nondeterministic selection for integer variables and a committed location are added to the model manually.

• •

Gate can be Free Occ and it is initially Free.

• •

Gate can send Go and go from Free to Occ.

• •

If Appr is received, then Gate can go from Free to Occ.

• •

If Leave is received, then Gate can go from Occ to Free.

6.3 Specifications for the whole model

Below, we give some useful specifications and their resulting UPPAAL queries.

• •

It might eventually be the case that for Gate, Occ holds:E<> Gate.Occ

• •

For Gate, Free holds leads to for Train, Cross holds: Gate.Free --> Train.Cross

• •

It shall always be the case that for Train, Cross does not hold or for Gate, Free does not hold: A[] not Train.Cross or not Gate.Free

• •

Deadlock never occurs: A[] not deadlock

• •

For Gate, Free shall hold within every 40: A[] not Gate.Free or y <= 40

Notice that, in Gate TA, clock y does not exist in the original example of UPPAAL. Since the last specification has a timing condition, it is generated automatically to verify the specification.

7 Conclusion

In this paper, we presented a new method for assisting TA construction and a tool implementing this method. ATAC constructs TA models and generates queries from high-level descriptions and specifications given in structured natural language. Output models and formulas can be imported to UPPAAL for verification. We gave a brief introduction to the basic concepts of TA and UPPAAL, and then presented description and specification grammars. Finally, we presented a case study generated with ATAC . Additional examples are included in the tool [20]. Although our method can be used for construction of a complete TA along with queries for specifications, we suggest using it as an assistance tool rather than a fully automated one. We encourage using it in the initial phases of the design where only a textual description of the model under construction is available. This way our method can provide an almost complete model which can be further improved. In addition, it identifies the necessary number of clocks and allocates them on the TA model for the considered RTS. Furthermore, accompanying the model with the specifications and descriptions given in natural language improves its maintainability.