|
Overview
Model based system testing
is an important tool for a system designer. If the designer
can verify the behavior of his system and knows about the
performance before actually building the system, that is the
best leverage to expect out of such model-based
testing. However, to be entirely useful, we need information
about all possible behaviors of a system. Hybrid systems have
continuous state space, which is
why to test the system entirely, we would need infinitely
many tests. This would make using testing for hybrid systems of little
use.
However, in HSCC '07, A.A. Julius, G.
Fainekos, M. Anand, I. Lee and G. J . Pappas
presented a novel idea of 'robust' testing of hybrid system,
where, given a hybrid automaton model and a sample simulation
trajectory, their algorithm could not only talk conclusively
about the safety of that trajectory, but also about a robust
neighborhood around it. What it meant is that if another
trajectory were to start from the same neighborhood around the
original initial conditions, it would follow the same
qualitative behavior at least until the time the original
trajectory was checked for safety. With this jump from being
able to talk just about an infinitesimally small initial
condition to a finite nonzero area of possible intial
conditions, we feel this algorithm can be used more
extensively to test hybrid systems.
====================================================================================================
STAGE I - Defining a hybrid automaton - Up and running
The process
of generating a hybrid automaton model is
three-fold.
- Step 1
: Create a vector of locations - 'loc'
instances
- Step 2 : Generate a skeleton (without
any edges at this point) of the
automaton
- Step 3 : Add
information about the edges
This could be achived by
writing a program to construct an automaton, which is
currently up and running, or by using a hybrid automaton
constructor GUI, which will be available soon.
Generating a hybrid
automaton model programatically:
- Step 1
: Create a vector of locations - 'loc'
instances
- Generating a 'loc' instance
- A location has an invariant,
some dynamics, and an optional name.
- The type of invariant set supported currently is of
the type 'polytope'. You will
need to have the multi-parametric toolbox installed in
Matlab for this. Generate a polytope instance.
(Type 'help polytope' at the Matlab prompt for more
information on how to create a polytope instance.)
- The types of dynamics supported currently are:
'constant' (x_dot = constant),
'timed' (x_dot = 1, a
vector of all 1s, special case of constant dynamics),
'affine' (x_dot = Ax+b, where A
and b are the matrix and the vector of correct
dimensions) and 'nonlinear'
(x_dot = f(x,t),
where f is a of
the class 'function_handle')
- The name
is optional and if you decide to enter one, then it must
be of the type 'character'.
- In addition, each location
instance has two (at most one of which could be 'true'
at any time) flags 'goal' and
'unsafe', depending on whether a
particular location is a goal location or an unsafe
location.
- You can try creating 'loc'
instances if you have already
downloaded the toolbox, unzipped it and included in your Matlab
path. Type 'help loc ' to
get help. Try creating loc instances using the function
'loc.m'.
- If you need to see an example, see
how 'loc' constructors have been used inside the file
'generatehscc1.m'.
- Combine the loc instances in a
vector.
- Step 2 : Generate a skeleton (without
any edges at this point) of the
automaton
- Generating an 'ha' skeleton from a
vector of 'loc' instances
- Generate a hybrid automaton
skeleton using the function 'ha.m'. Type 'help ha' to get help.
- As an example, you
can refer to 'generatehscc1.m'. Type 'help generatehscc1' to get
help on that function.
- Step 3 : Add
information about the edges
- Adding edges to the skeleton you
just made
- Use the function 'addedge.m' to
the hybrid automaton instance you created in the earlier
step. Type 'help
addedge' to get help.
- As an example, you
can refer to 'generatehscc1.m'. Type 'help generatehscc1' to get
help on that function.
- Once all your edges have been
added, your 'ha' instance is
all-powerful.
Using a GUI to do
generate a hybrid automaton model:
*coming soon* (The GUI is
currently under development.)
Scroll down for a
screenshot of a concept-level GUI. Functionalities are being
built in.
====================================================================================================
STAGE II - Generating simulations on the
hybrid automaton objects - Up and
running
-
Once we have a complete 'ha' instance, we can
simulate its dynamics.
- We
need to provide the 'ha' instance,
time span for simulation, initial location and initial conditions
for the
continuous state variables.
- Type 'help
@ha/simulate
'
to get help.
- For the purpose of
simulation of the dynamics, all types of dynamics are
supported, including nonlinear dynamics. [However, if the
user wishes to generate robust neighborhoods (STAGE III),
then nonlinear dynamics will not be supported.]
- As an example, one legal
function call for simulating an 'ha' instance for the 3x3
HSCC navigation benchmark problem could be:
h =
generatehscc1; % Create an 'ha' instance for the 3x3 HSCC
Navigation Benchmark problem
t_span = [0 1];
% Time span for simulation of the
dynamics
init_loc = 5; %
Initial location
init_cond =
[1.5, 1.5, 0.5, 0.5]; % Initial
conditions
traj =
simulate(h,t_span,init_loc,init_cond); % Function call for
the simulation
-
Try other combinations of 'ha'
instances, time spans, and initial location &
conditions.
- Results
- Here is a comparison between the
simulation results for the 3x3 HSCC
Navigation Benchmark problem proposed in the
HSCC 2004 paper
(left) and the simulation
results that were obtained using the toolbox (right).
|
Navigation Benchmark
problem - Example from the paper
|
Navigation Benchmark problem - Simulation
results using the
toolbox
|
====================================================================================================
STAGE III - Generation of robust
neighborhoods, given a trajectory -
Up and running
-
If
you could successfully generate a trajectory using the
simulate function, you would have known whether the
trajectory was definitely safe, definitely unsafe, or
safe-until-the-time-horizon-specified. We are most
interested in the third case - safe until the time horizon
specified.
-
Given the part of the trajectory that is
safe until the time horizon specified, we are interested in
being able to build neighborhoods along it, with which,
we can certify the behaviour of any other trajectory that
passes through those neighborhoods. In particular, we
look to certify that any other trajectory that passes all
the way through this robust 'tube' generated by the
neighborhoods, will not only be safe until the time horizon
specified, but will also follow the same qualitative
behavior (passing through the same set of locations and
crossing the same guards).
- Robust neighborhood
generation is currently not supported for ha instances that
might have locations with nonlinear dynamics.
-
-
Results:
-
Following are a few examples
of the
robust neighborhoods generated, given a hybrid automaton
for the 3x3 HSCC benchmarks model and
a sample simulation trajectory. They provide a screenshot
of the final tube that gets
generated.
-
*NEW*If you wanted to see the step-by-step
progress of the tube generation code, download/watch the
movie. (Caution:
Large size - ~160 MB. May be it's better to save the movie
on your local drive before playing.)
-
Notice
the ellipsoidal (elliptical in 2-D) tube generated along
the trajectoy that lies at the
center.
-
Notice how
the flow inside the cyan tube (central square)
'funnels' into the magenta tube (middle-right
square).
-
Not only is the trajectory at the
center of this tube safe, but so is every other trajectory
that starts within the first cyan
ellipsoid, until the time for which we have
the robust tube (the specified time
horizon).
-
Also note that if a trajectory, for
some reason, does not enter into the magenta ellipsoid,
it could possibly hit the lower guard (x = 1) in
case of example 1, and upper guard (x = 2) in case of
example 2. However, if any trajectory ends up
starting inside the magenta tube, we can vouch that
it will be safe at least until it comes to the
end of the tube. < /DIV >
<
/DIV >
|
Example 1 |
Example
2 |
====================================================================================================
STAGE
IV - Development of a GUI - Work in progress
-
Results so far:
- Here is a one possible draft version of how the constructor GUI
for class ha *might* look. Click for a more detailed view.
====================================================================================================
Creating installation notes, user manual, examples -
To be done
|
