#!/usr/local/bin/php MoBIES: University of Pennsylvania

MoBIES Project
DIVES: Design, Implementation, and Validation Of Embedded Software
 
:
(internal use only)
 

Maintained by
Insup, Oleg, Valya
July 20, 2000

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:

    1. Unpack the tools
    2. Go into the generated directory called "CharonCP"
    3. To start CHARON, run the following command depending on your operating system:
      • Windows: run-charon.bat
      • Unix: run-charon.sh
    4. The CHARON manual can be downloaded here: manual.ps
    5. 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.
    6. 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.