Affiliations: Department of Electrical Engineering, National Taiwan
University, Taipei, Taiwan 106 | Institute of Information Science, Academia Sinica,
Taipei, Taiwan 115
Abstract: We introduce the symbolic simulation function implemented in our
model-checker/simulator RED 4.0 for dense-time concurrent systems. By
representing and manipulating state-spaces as logic predicates, the technique
of symbolic simulation can lead to high performance by encoding even a dense
amount of traces in traditional simulation into one symbolic trace. Symbolic
simulation adds the dimension of width to a trace of state-spaces. By
controlling the width of traces, we have a much better chance to find bugs
using fewer traces. Our main contribution is the design of symbolic simulation function
in RED 4.0 for dense-time concurrent systems. In our tool, users can strongly
control the width of traces and the generation of traces. We discuss how to
generate traces using various policies, how to manipulate the state-predicate,
and how to manage the trace trees. Moreover, we design a C-like language whose
programs can be mechanically translated into the optimized communicating timed
automata(CTA). Engineers can also put down comment-line assertions as
specifications in their verification tasks. Finally, experiments using our
simulator to verify the Bluetooth baseband protocol justify the usefulness of
our tool. The tool is available at http://cc.ee.ntu.edu.tw/~farn/.
