Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

る考察

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

from Timed Automata to Timed Modules

Yoshinobu Tachi

School of Information Science,

Japan Advanced Institute of Science and Technology

February 15, 2001

Keywords: timed automata, timed modules,real-time systems, software process.

1 Background

For real-time systems, such as communication systems, logic circuits, operating systems

etc., wemust ensure not onlythatthey workcorrectly butalsothat they work incorrect

timing. Recently, many real-time systems are very large and complex, so that it is very

diÆcult to verify correctness of them by simulation tests. Hence, we need mathematical

verication methodsin the design step of them.

For this purpose, that is, for verication of correctness of real-time systems, timed

automata and timed modules are proposed. The timed automata model is an extension

ofawell-known model,automata. Eachtimedautomatonhas clocks tocontrolitstransi-

tions: eachedge of atimed automaton may have clock constraints and clock resets. The

timed module model is the model which describes systems by transitions of the values

of variables. The types of variables are discrete(boolean or enumerate) and clock(real).

That is,by using this model, wecan treat both actions concerningdiscrete variablesand

action concerning clocks by the same manner. Both of the two models are proposed by

Alur et. al. They suggests that the timed module modelis a generalizationof the timed

automata model. However, they did not explicitly give any transformation procedure

fromtimed automata to timedmodules.

Copyrightc 2001byYoshinobuTachi

Modules

Then, in this thesis, we give a transformation procedure from timed automata totimed

modules. The procedure consists of the followingtwosub-procedures.

An equivalent transformation procedurefrom timedautomata to timed modules

Anoptimizationprocedure for the timedmodules obtainedby theabove procedure

Wealsogivetheproofsof thevaliditiesof them. Notethatthe procedureisforthetimed

I/Oautomatamodel. ThisisthemodelwithInput/Outputdistinguishintheevents. We

use this model becausesystems and processesthat wewant todescribeneed suchevents.

Weapply this procedureto the following two examples.

A specication of a train/gate controller system

(This is anexample of real-timesystems.)

\Software Process Modeling Example Problem"by Kellner et. al. [3]

It isone feature of this thesis thatwegiveasoftware process description inanautomata

model. Wehavecomparedthedescriptionobtainedby theprocedurewiththedescription

in timed automata, for both examples. We conclude that the descriptions obtained by

applyingthe procedure are certainlyoptimized. This isdue todiscretevariablesoftimed

modules, which giveus exible descriptions. Details are shown in the next section.

3 Comparison between Two Models

Because only one event are allowed to occur for each transition in timed automata, we

need towrite descriptions whichare not simple,in the followingcases.

Forthecasethataneventcanoccuronlywhensomeotherinputeventshavearrived,

we need the same number of edges and states asthe number of the input events.

Itissimilarfor thecase thatanevent canoccuronlyaftersomeoutputevents have

occurred.

For each of the above cases, if the order of the input(output) events can not be

determined, then the number of the possible orders is the factorial of the events,

and we need the same number of states and edges as the number of the orders.

For an input event and a continuously succeeding output event, we also need two

edges and states.

Suppose that we need a judgment in a description. We need the same number of

states and edges asthe number of the results of the judgment.

\resetevent"ofanotherautomaton. Weneedthesamenumbero9fadditionaledges

as the number of the states of the automaton.

By using timed modules, we can write simpler (optimized) descriptions for each of the

above cases.

In timed modules, each input event is expressed by the assignment of \true" for

the boolean variable corresponding to the event, as a condition of an expression.

Hence, we can describe the arrivalsof many input events by the conditions of only

one expression.

It is similarfor the case of outputevents.

In timed modules, the order of events becomes the order of the conditions of an

expression. Because we need not consider this order, we need only one expression

alsofor this case.

Aninputeventbecomesaconditionof anexpression andacontinuouslysucceeding

output event becomes an assignment in the expression. Hence, we need only one

expression alsoforthis case.

Intimedmodules,theresultsofajudgmentareexpressed bythevaluesofavariable

with enumerate type. Hence, weneed only one variablefor any judgment.

For a \reset event", we must add only one expression which lets the value of the

variable \state" be the value denoting the initialstate whenever the current value

of the \state" is.

In the examples in the chapter 4, we have shown the optimized descriptions in timed

modules obtained by applying the abovemethods. Notethat descriptions intimed mod-

ules are sets of expressions, sothat they are not easytoread. Hence, we alsopropose an

\automata representation" of timed modules, inthis thesis.

4 Future Works

Future works are as follows.

1. Application of the transformation procedure to other examples, that is, other ex-

amples of real-timesystems and other software processes.

2. Development of furtheroptimization methods.