Download INSTITUT F¨UR INFORMATIK CASE Tools for Embedded Systems

7.2. MODELING THE SYTEM
103
for the requirements elicitation, because they support the developer in the analysis of complex systems, and for its validation
and verification after the developing process.
• Then we have data type definitions (DTDs, see Section 7.4, "Model
of the Controller") which can be defined in J AVA or Q UEST F.
When starting a new model, the developer has the choice of
which programming language to use. If you take Java, a partial
set of basic types of the Java programming language is available
for typing, but user-definded types are not allowed. Therefore
the models are sometimes difficult to understand. QuestF as a
functional language allows such types besides Bool, Float and
Integer by means of data constructs, so that channels and ports
can have types which are self-explanatory. User-defined auxiliary functions can also be built in QuestF and even constants
can be defined. The concept of the DTD using Q UEST F is very
powerful and gives the experienced developer a very powerful
instrument at hand, to develop own data type and corresponding functions for the design of the model.
• At last A UTO F OCUS provides the concept of state transition diagrams (STDs, see Section 7.4, "Model of the Controller"), which
is similar to state charts diagrams, known from the UML modelling language. Each STD can be assigned to one or several
SSDs. In such diagrams there are different states which can be
initial, final, both or just regular states. Beginning with the initial
state another state can be reached with a transition. A transition
takes different arguments, which can be:
–
–
–
–
–
precondition
input port
output port
postcondition
priority
The input ports specified, define on the one hand data, wich
can be used in preconditions or written to an output port. On
the other hand the pure presence or absence of a value can be
checked as well. A transition can consider preconditions for the
input values or local variables stored in the appropriate SSD.
It also can define postconditions for the local variables which
means that those variables have to adopt new values. At last,
the priority of the transition is a instrument to make a STD deterministic, because it can be defined, which transition is used,
if there are multiple choices. This is very useful, if you have to
consider special cases.