Case Study
We now provide an example for showing the usage of MIST. using MIST. The example is a model-based embedded software which makes a robot to chase a bright object. This program was generated from a CHARON model automatically using CHARON to C++ code generator. Our goal is to use MIST to enhance the model with runtime verification and perform both design-leve and implementation-level validations.
The targeted hardware is a SONY robot dog AiBO. AiBO has a MIPS processor and a collection of sensors and actuators which enables this dog to walk, to see, and to move its head etc. The model-based software we study is to control the movement of the dog head. Figure 1 shows the hybrid model for this control software. It takes two input variables: visibility and the angle between the ball and the dog head. When the visibity is greater than a threshold, say, 10 in our case, the model switchs to the rightmost mode and the dog's behaviour, indicated by the differential equations in the model, will make the dog to move its head toward the ball. The CHARON model of dog head can be found here. The original model, provided by the courtesy of Dr. Jesung Kim, is enhanced by a tester, which mimics the movement of a ball.
Figure 1. The hybrid model for controlling dog head.
Next, we write the property we wish to monitor. In our case study, the property we are interested in is that, if the dog loses the ball 50 seconds after the ball becomes visible, an alarm should be raised. The MEDL script for this safety property can be found here. The mPEDL script for instrumenting the model can be found here.
Now, use the P2C to instrument model as below,
localhost> p2c -i dog.cn dog.pedl
You should have an instrumented model file dogInst.cn similar to this.
Use the M2C to synthesize the runtime checker and add it to the instrumented model,
localhost> m2c -i dogInst.cn dog.medl
You should have a file called dogInstMon.cn, which is an instrumented model and comes with a model-based runtime checker.
Design-level validation
For the design-level validation, you can simulator dog.medl on the CHARON toolkit. Important: you need to put Events.class and EventElement.class to your charon\user directory. You may want to choose the following simulation parameters:
- Simulation Step Size: 0.1
- Total Steps: 2000
Here is the some snapshot of simulation trace,
Figure 2. The movement of a virtual ball.
Figure 2 shows the movement of a virtual ball. Note that the visibility of the ball is below the threshold in the initial 10 second, and hence any movement of the dog head should not be counted as "losting a ball". The speed of the ball also increases during the course.
Figure 3. The angle between the ball and the dog head
Figure 3 shows the angle between the ball and the dog head. Note that with the ball's speed increasing, it gets harder and harder for the dog to chase the ball.
Figure 4: The alarm lostTrack is raised
An alarm is declared by the value change of its related time variable. In this case, an alarm is detected at the second 66. Note that the dog also lost its ball at the second 10, the time when the ball becomes visible, and such event is intentionally omitted by the runtime checker, because we allow 50 seconds for the dog to establish its movement after the ball becomes visible.
Implementation-level validation
The self-monitoring model can be further translated to the executable code by following the existing model-based code generation path. It could be done manually or automatically, depending the available mechinism for code generations. In our case study, we use the Charon to C++ code generator developed by Dr. Jesung Kim. Since we are not able to directly observe the value of losttrack_time, we instead link it to a function call: whenever there is a change on lostTrack_time, we simply let dog bark or flash some lights. For more information about Charon to C++ code generator, you can contact Dr. Jesung Kim. We hope that we can post some video clips about our experiments soon.