Information Technology Reference
In-Depth Information
and for all valuations
ρ
:
X
→U
while universal validity
π
of a transition
predicate
π
∈T
(
W
,X
)meansthat
π
is valid for any two data states and any
valuation.
The above definitions are generic and sucient for the following considera-
tions. Therefore, we do not fix a particular syntax for signatures and predicates
here, neither a particular definition of the satisfaction relation. We claim that
our notions could be easily instantiated in the context of a particular assertion
language. How this would work in the case of the Object Constraint Language
OCL is shown in [5].
Example 2.
We exemplify the use of signatures in our running example. The
component
Leg
has the I/O-signature
Σ
Leg
=(
V
Leg
,
O
Leg
)where
V
prov
Leg
}O
prov
Leg
=
{
maxStep
,
currStep
=
{
init
()
,
lift
()
,
swing
(
a
)
,
drop
()
,
retract
()
}
V
req
Leg
O
req
Leg
=
{}
=
{
update
(
a
)
}
V
int
Leg
O
int
Leg
=
{
steps
}
=
{}
Leg
has as provided state variables
maxStep
, which models the maximal step size,
and
currStep
for the current step size of the leg. The only internal state variable
is
steps
which counts the number of steps the leg has made since initialization
(provided operation
init
()). The provided operations also include operations for
the different kinds of leg motion, i.e.
lift
(),
swing
(
a
),
drop
(), and
retract
(); the
only required operation is
update
(
a
) which, after a step has made, informs the
leg controller component
LegC
about the actual step size. A (
V
prov
Leg
∪V
int
)-data
Leg
V
prov
Leg
∪V
int
state can be given, for instance, by the function
σ
:(
)
→U
with
Leg
σ
(
maxStep
)=50
,σ
(
currStep
)=0
,σ
(
steps
)=5.
The controller
LegC
has the I/O-signature
Σ
LegC
=(
V
LegC
,
O
LegC
), where
V
prov
LegC
V
req
LegC
V
int
LegC
.The
provided state variable
distance
stores the total distance to be walked by its (con-
nected) leg, the internal state variable
gone
models the distance that has already
been moved by its leg. The meaning of the required state variables
maxStep
and
currStep
has already been explained above. The provided operations of
LegC
in-
clude
update
(
a
). In the following, for the specification of the behavior of
LegC
,
we will only consider transitions labeled with
swing
(
a
)
=
{
distance
}
,
=
{
maxStep
,
currStep
}
,and
=
{
gone
}
∈O
req
LegC
(which is a
provided operation of the
Leg
component, hence shared with
LegC
).
We are now able to define which labels can occur in a modal I/O-transition
system with data constraints. Given an I/O-signature
Σ
=(
V
,
O
L
(
Σ
)
), the set
of
Σ
- labels consists of the following expressions:
∈O
prov
a provided operation,
ϕ
V
prov
,par
(
m
)) the
1. [
ϕ
]?
m
[
π
]with
m
∈S
(
V
prov
∪V
int
,par
(
m
)) the postcondition,
precondition,
π
∈T
(
∈O
req
a required operation,
ϕ
V
prov
∪V
req
∪V
int
,par
(
n
))
2. [
ϕ
]!
n
[
π
]with
n
∈S
(
V
req
,par
(
n
)) the postcondition,
the precondition,
π
∈T
(
∈O
int
an internal operation,
ϕ
V
prov
∪V
req
∪V
int
,par
(
i
))
3. [
ϕ
]
i
[
π
]with
i
∈S
(
V
prov
∪V
int
,par
(
i
)) the postcondition.
the precondition,
π
∈T
(
Search WWH ::
Custom Search