Dr. He is collaborating with Dr. Hong Zhu at the Oxford Brookes University in England in developing a theory for testing concurrent software systems. This research is partially supported by the National Science Foundation under grant # INT 9731620.
We have developed a general theory of testing concurrent software systems and a method for testing high-level Petri nets. We used a complete partially ordered set notation to formally define a proper behavior observation and recording scheme and the desirable properties (also called assumptions) the scheme needs to satisfy.
Let N be a predicate transition net, M0 be the set of initial markings of N, M0 is thus the set of test cases for N. An execution of N on test case m0 is a sequence of reachable markings starting from m0 and linked by transition firings. We denote such an execution as follows: 
, where ni are transitions, m0Î
M0 is an initial marking, mi, i=1,2,…, are markings such that mi is obtained from mi-1 by firing transition ni.
Complete Scheme of Behaviour Observation
The complete scheme y
N =(
, Y
N) of observable behavior and a recording function Y
N of a given predicate transition net N is inductively defined as follows:
- Let
= {e | e is an execution of N on m} for all mÎ
M0, 
, 
(the power set of RN). The partial ordering £
Y on the set of observable behavior is the set inclusion relation Í
. - For all mÎ M0, Y N({m})={{e} | eÎ RN,m}.
- For any test set M Í M0 and mÎ M0, Y N(M È {m})={uÈ {e} | uÎ Y N(M) Ù eÎ RN,m}.
Intuitively, the complete scheme of behavior observation records every detail of the executions of a concurrent system.
We proved the subsuming relationships among various proposed testing adequacy criteria shown in the following Figure.
Currently, we are adapting the above results to test software architectures defined in SAM.
For problems or questions about this web, contact webmaster@cadse.cs.fiu.edu