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