Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Model Checking via Reachability Testing
The computational engine of the verification tool Uppaal
consists of a collection of efficient algorithms for the analysis of
simple reachability properties of systems. Model checking of
properties of (networks of) timed automata other than plain
reachability ones may currently be carried out in such a tool as
follows. Given a property F to model check, the user must provide a
test automaton Test(F) for it. The test automaton must be such that
the original system SYS has the property expressed by F precisely when
none of the distinguished reject states of Test(F) can be reached by
the agent obtained by making the test automaton interact with the
system under investigation. This raises the question of which
properties may be analyzed by Uppaal in
this manner.
The aim of this project is to provide such a characterization for the
model of timed automata used in Uppaal, to
experiment with different notions of parallel composition describing
the interaction between testers and tested systems, and to implement
the test automaton construction. The interested students are invited
to look here for
an introduction to the theoretical foundations of such a project.
Luca Aceto,
Department of Mathematics and
Computer Science,
Aalborg University.
Last modified: Wed Nov 27 15:10:32 1996