|
RefChecker is a model checker, or state space
exploration tool, for systems with highly dynamic
structure, in the sense that the way components are
connected is dynamic and can change over time.
Formal models such as state charts or
Petri nets are used to model and analyse
the dynamic behaviour of concurrent systems. In the
basic form, these models has a static "program
description", in the form of a net or a state
machine, and dynamic states, in the form of current
states or token distributions. The dynamic aspects
are, so to speak, kept in data, while the data
manipulation is done by static programs.
Contrast this to Object Orientation, where
data and program is integrated, and where programs
manipulating data is replaced with objects
interacting. The data, being manipulated in one
object's program, is other objects, each with its own
internal program.
While "static program" models in many cases
suffices, when modelling agents and
mobility encoding objects in data becomes
cumbersome, and more dynamic modelling languages are
needed.
State space exploration of formal models
has proven to be a successful analysis technique.
The basic idea behind a state space is intriguingly
simple. One construct a directed graph, which has a
node for each reachable state and arcs corresponding
to state transitions, and from this graph it is
possible to algorithmically analyse and verify a
large number of properties of the system.
Model checking systems with dynamic structure is
further complicated, compared to the static
structure models, by the references between objects.
A state can no longer be seen simply as a
distribution of data-tokens, say, but the entire
reference graph needs to be taken into consideration
(one object references another, who in turn
refernces a third that refers back to the first
etc.)
The RefChecker tool is aimed at handling these kinds
of dynamic structures, using an explicit
representation of the reference graph, and using
graph isomorphism algorithms to compare states to
avoid representing equivalent states.
|
