|
Midterm Experiment
Tools
- CHARON: This CHARON tools for hybrid system modeling can be downloaded from here: charon.tar.gz.
(This release does not include the
Visual Editor for CHARON.)
Instruction: To use the tools, please do as follows:
- Unpack the tools
- Go into the generated directory called "CharonCP"
- To start CHARON, run the following command depending on your operating system:
- Windows: run-charon.bat
- Unix: run-charon.sh
- The CHARON manual can be downloaded here: manual.ps
- Warning:
- Netscape 3.* and 4.* on some versions of Windows will corrupt jar files.
- Depending on your settings of environment variables, you may experience an error when generating simulator on some Windows platforms. The error results in the error message "CreateProcess error=2". If this happens, make sure that "javac.exe" can be found via your system-wide class path. You can also compile the simulator manually by running:
javac CHARON\simulator\<projectName>gSim.java
where <projectName> is the name of your project.
Before running <projectName>gSim manually, the directory for saving the traces should be created under "CharonCP":
mkdir traces.
Then execute java byte-code interpreter:
java CHARON.simulator.<projectName>gSim.
- Please consult the CHARON webpage for further information about the tools:
http://www.cis.upenn.edu/mobies/charon/
and e-mail charon-dev@saul.cis.upenn.edu
if you find problems running the tools.
- Predicate Abstraction
The above CHARON tool also includes the predicate abstraction tool as an executable file for the linux systems.
To start the predicate abstraction tool:
- Go into the "CharonCP" directory
- Type at command line:
boolreach_i686 <filename.hyb>
Reports and Presentation
Examples
- Thermostat:
- thermostat.cn: This CHARON file was used during the mobies netmeeting presentation on Feb 27th, 2002.
- thermostat.hyb: This file contains the CHARON model translated to the input language for the predicate abstractor.
- addThis.hyb: This file is the additions to the thermostat.hyb file. It needs to be added before we can start the predicate abstraction tool.
- thermostat.par: The corresponding parameter file for the thermostat example.
- Platoon:
- platoon.cn: The CHARON file with the platoon longitudinal controller.
- platoon.par: The parameter file for the predicate abstraction tool for the platoon.cn example.
Help
Interpreting the textual output of the predicate abstraction tool
As the predicate abstraction model checker is still a prototype version,
there is not enough documentation about the tool yet. This is particularly
true about how to interprete the textual output of the tool. We will use the
aforementioned thermostat.cn
example to give a brief overview.
Adding the initial region, the bad region and the limit set as described in
addThis.hyb, the tool will produce the following output file:
thermostat.txt.
The most important output is the last line, stating that the predicate
abstraction tool found that the property holds (that means, the bad region is
never reached from the initial region). The second to last line specifies the
number of reachable abstract states, namely 29. The preceding lines give all
the states found in the order they were reached. In addition, the output
specifies how we found this new state (it is either an initial state, or it is
discovered by continuous flow of time, or by a discrete jump between modes or
locations), and from which state it was reached. An abstract state consists of
two parts: its location and the truth assignment to the k predicates used
during the predicate abstraction. Loc 0 refers to the mode Heat in the
thermostat.cn file (see the automatically generated
thermostat.hyb file), Loc 1 to the mode Check, and Loc 2 to the mode
Cool. The following string of T's (true) and F's (false) refers to the k
ordered predicates. The ordering of the predicates is given at the beginning of
the file (see the line "The initial predicates are:"). Hence, the line "New
state (Loc 0, FTT TTF FFF) is an initial state!" stands for the concrete
continuous region 6 < Temp < 9, clock < 0.5, in the Heat mode.
As we limit our state space for the clock to be between 0 and 10,
clock < 0.5 means 0 <= clock < 0.5.
This picture
represents the graph of discovery of new abstract states that corresponds to
the textual output thermostat.txt.
We included a running number for each state, which corresponds to the
chronological ordering of the reachable states in the textual output. Dashed
arrows correspond to transitions between abstract states that are taken due to
continuous flow of time, whereas solid arrows represent transitions due to
discrete jumps between modes or locations. Please note, that we are not trying
to compute all possible arrows in the graph, but we are trying to compute all
reachable states. Hence, we only include arrows that represent the first time a
new abstract state is found. Also, for brevity reasons, we use T instead of the
name temp, and t instead of clock in the picture.
If you change the initial region for this example, so that the clock starts
with a value that is bigger than 2, then the predicate abstraction tool will
find a violation of the property. If you change the line following the keyword
"initset" from
"<= 0.0 1.0 -0.1 , /* clock - 0.1 <= 0 */"
to
" >= 0.0 1.0 -2.0 , /* clock - 2.0 >= 0 */"
then the following textual output will be generated: error.txt.
The difference here is that the predicate abstraction tool finds a
counter-example to the property (that is, a trace from the initial region to
the bad region). The lines following "Stack content" represent the
counter-example. Again, we need to translate the counter-example trace into the
concrete state space. Please note, that this counter-example might not be valid
in the concrete state space. If the user analyzes the counter-example and
determines that it does not correspond to a real counter-example in the
concrete state space, new predicates may be added to predicateset that may
eliminate this case. We are currently implementing a tool that will generate
new predicates for the user, but as of now, the analysis has to be performed
manually.
|