Information Technology Reference
In-Depth Information
natural manner. Moreover, we revise the algorithm of [WL05] to work for TLCE-
based symbolic test generation, and present experimental results to demonstrate
the effectiveness of our approach.
The rest of the paper is organized as follows. Section 2 presents TLCE with
its syntax and semantics. The TLCE-based symbolic test generation algorithm
is introduced in Section 3. Section 4 illustrates a case study on a cache coherence
protocol. The paper is concluded with Section 5.
2
A Temporal Logic with Constrained Events
We presuppose the following syntactic categories:
Val
is a set of values ranged
over by
v
;
Var
is a set of variables ranged over by
x, y, z
; a valuation is a total
mapping from
Var
to
Val
, denoted by
ρ
; a substitution
v/z
maps
z
to
v
.Let
b
range over boolean expressions over
Val
Var
,and
c
over channel names. The
syntax of TLCE is given by the following BNF-definition:
∪
β
::=
c
?
z
c
!
z
η
::=
G
ϕ | ϕ
U
ϕ
ϕ
::=
tt |¬ϕ | ϕ ∧ ϕ |
E
η |
A
η |β
:
bϕ |
[
β
:
b
]
ϕ
|
TLCE can be seen as a first-order extension of CTL [CGP99]. The operators
specifies an input event on channel
c
such that the received values, to be stored
in the variables
z
,satisfy
b
; similarly,
β
:
b
and [
β
:
b
]are
constrained input/output modalities
.Intuitively,
c
?
z
:
b
says an output event must occur
on channel
c
such that the output values, stored in the variables
z
, satisfying
b
.
The semantics of TLCE is defined over a labeled transition system as follows:
c
!
z
:
b
ρ
There exists a
s
Val
|z|
s
c
?
z
:
b
ϕ
∈
S
such that for any
v
∈
c
?
v
−−→
s
and
s
M
ρ{v/z}
(
ρ
{
v/z
}
b
),
s
ϕ
.
ρ
There exist
s
Val
|z|
s
c
!
z
:
b
ϕ
∈
S
and
v
∈
(
ρ
{
v/z
}
b
)such
c
!
v
−−→
s
and
s
M
ρ{v/z}
that
s
ϕ
.
c
?
v
−−→
ρ
[
c
?
z
:
b
]
ϕ
For any
s
∈
Val
|z|
(
ρ
s
,then
s
S, v
∈
{
v/z
}
b
), if
s
s
M
ρ{v/z}
ϕ
.
ρ
[
c
!
z
:
b
]
ϕ
For any
s
Val
|z|
s
∈
S
,ifthereexists
v
∈
(
ρ
{
v/z
}
b
)
c
!
v
−−→
s
,then
s
M
ρ{v/z}
such that
s
ϕ
.
ρ
ρ
ϕ
.
s
¬
ϕ
s
ρ
ρ
ρ
s
ϕ
1
∧
ϕ
2
s
ϕ
1
and
s
ϕ
2
.
ρ
E
[
G
ϕ
]
s
There exists a path
π
from
s
such that for all
j
≥
0,
ρ
ϕ
.
s
j
s
ρ
A
[
G
ϕ
]
For every path
π
from
s
and all
j
≥
0,
s
j
ρ
ϕ
.
ρ
E
[
ϕ
1
U
ϕ
2
] There exists a path
π
from
s
and a
k
s
≥
0 such that
ρ
ϕ
2
and for all 0
ρ
ϕ
1
s
k
≤
j<k,s
j
ρ
A
[
ϕ
1
U
ϕ
2
] For every path
π
from
s
,thereexistsa
k
s
≥
0 such that
ρ
ϕ
2
and for all 0
ρ
ϕ
1
s
k
≤
j<k,s
j
Search WWH ::
Custom Search