Using Timed Finite Automata to define the timing behaviour of a system

In embedded systems the functionality of software is usually tied in some way to timing deadlines. Specifying systems when there are many software components working together can be challenging or impossible. Many customers we have worked with would like to be able to specify things more accurately during the requirements stage of system design.

Timed Finite Automata is one of the notation options available to them. Timed Finite Automata are very similar to a Deterministic Finite Automaton, in that they contain a finite number of states and a number of transitions between those states (including cyclical transitions).

Figure 1: Deterministic Finite Automaton (DFA)

This is an example of a Deterministic Finite Automaton. Transitions leading to the green ‘OK’ state are allowed, transitions leading to the red ‘NOK’ state are erroneous.

TFA allows additional timing constraints to be added to the transitions, as shown in the diagram below:

Figure 2: Timed Finite Automata (TFA)

In this example the transition from S1 to S2 now needs to happen in less than 10 time units. In this notation T is the current time and S1.T is the time recorded on entry to the S1 state. If this transition happens in less than 10 units of time and is followed by the ‘C’ input then the OK state will be reached. However, if the transition takes more than 10, or is not followed by ‘C’ then NOK state will be reached.

At the requirements or design stage of a project this can be used to assign budgets to software components. Pairing timing budgets in specifications with the use of RapiTime will help identify potential timing pinch points much earlier in the development process. Being made aware of these issues and the need for optimisation or a more powerful microprocessor long before the integration stage will certainly help keep the costs of such mistakes down.

This work is part of research performed within the PRESTO project (ARTEMIS-2010-1-269362), a research project co-funded by the European Commission under the ARTEMIS Joint Undertaking Programme. More information can be found at http://www.presto-embedded.eu/.