Information Technology Reference
In-Depth Information
Symbolic Test Generation Using a Temporal
Logic with Constrained Events
Daguang Liu 1 , 3 ,PengWu 2 , and Huimin Lin 1
1 Lab of Computer Science, Institute of Software, Chinese Academy of Sciences,
Beijing 100080, China
2 CNRS and LIX, Ecole Polytechnique, 91128 Palaiseau Cedex, France
wu@lix.polytechnique.fr
3 Graduate School, Chinese Academy of Sciences, Beijing 100049, China
{ liudg,lhm } @ios.ac.cn
Abstract. A temporal logic with constrained event modallities, TLCE,
is proposed to represent test purposes for testing concurrent programs.
The logic is capable can express not only temporal relationships among
input and output events, but also data dependencies between event
parameters. A TLCE-based test generation algorithm is developed to
automatically derive symbolic test cases that incorporate given data de-
pendency constraints as verdict conditions. The advantage of the ap-
proach is demonstrated with a case study on a cache coherence protocol.
1
Introduction
The symbolic test generation method was proposed for the conformance testing
of reactive systems, where the models, test purposes and test cases are all rep-
resented as symbolic transition systems [RdBJ00, CJRZ02, RMJ04]. However,
only the temporal relationships among input/output (I/O) events are concerned
therein. This would result in less precise test cases, where the relevancy among
event parameteres are ignored. [JJRZ05] improved the method with an approx-
imate analysis on reachability/co-reachability. But in practice, it is still tedious
and error-prone to represent test purposes as transition systems.
A predicate sequencing constraint logic (PSCL) was proposed in [WL05] as
an alternative way to represent test purposes concerning data dependencies be-
tween event parameters. A PSCL-based symbolic test generation algorithm was
also developed there. The approach allows automated test generation based on
first-order temporal properties, and releases the effort in constructing transition
systems for test purposes.
This paper presents a temporal logic with constrained events (TLCE) which
refines PSCL, so that test purposes can be described in a simpler and more
The work of Peng Wu was partially supported by the INRIA/ARC project ProNoBis.
The work of Daguang Liu and Huimin Lin was partially supported by the National
Science Foundation of China under Grant No. 60421001.
Search WWH ::




Custom Search