We present an example, originally due to Jansen et al. in “A Probabilistic Extension of UML Statecharts”, but reinterpreted here. We consider a robot equipped with an idealised randomising device with two states that are equally likely to occur; the device generates an outcome from a flip
event in every time step. The robot uses the device to decide whether to terminate or to continue a particular activity (here, foraging). For reasons of its own, the robot may choose to ignore the outcome of the device. Finally, the robot considers only a limited number of times whether to continue foraging. We call this number N
and leave it loosely defined. Our simple modelling objective is to explore different values for N
that give us a high probability of terminating.
The RoboChart model is shown below.
The only state machine FgSTM defines a constant N
and a variable flips
. There are two states FORAGE
and STOP
in the state machine.
One possibility in the FORAGE
state is for the flip
event to occur and the robot to remain in the FORAGE
state; this models the robot ignoring the randomising device. The other possibility is available only if the number of choices has not been exhausted (flips < N
). In this case, the robot controller proceeds to a probabilistic choice between two equally likely alternatives. One alternative is to move into the STOP
state, which it signals with the stop
event; the other alternative is to return to the FORAGE
state, signalling this with the forage
event. In both cases, the controller keeps track of the number of choices made. Note that, if in the FORAGE
state flips < N
, then the behaviour is nondeterministic
: the robot controller might take either flip
alternative. There is only one transition available in the STOP
state: the flip
event keeps the controller in the STOP
state; this transition is included to model the fact that flip occurs in every time step, even when the controller has terminiated.
We use the probabilistic assertion language of RoboChart. The assertion language finally will be translated to the PRISM’s property langauge, but the assertion language is a more user-friendly way to verify probabilistic properties. Information about how to use the probabilistic assertion language can be found in RoboChart and RoboTool reference manuals.
Used configuration file.
The assertion file that is used for verification is shown below.
The verification results are displayed in the report below.
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
P_deadlock_free | foraging::foraging::stm_ref0::N=2 | 16 | 20 | 0.001 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=4 | 30 | 38 | 0.002 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=6 | 44 | 56 | 0.001 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=8 | 58 | 74 | 0.002 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.002 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=12 | 86 | 110 | 0.002 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=14 | 100 | 128 | 0.001 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=16 | 114 | 146 | 0.002 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=18 | 128 | 164 | 0.001 seconds | true |
P_deadlock_free | foraging::foraging::stm_ref0::N=20 | 142 | 182 | 0.001 seconds | true |
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
P_nonterminate | foraging::foraging::stm_ref0::N=2 | 16 | 20 | 0.007 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=4 | 30 | 38 | 0.011 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=6 | 44 | 56 | 0.013 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=8 | 58 | 74 | 0.012 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.012 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=12 | 86 | 110 | 0.019 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=14 | 100 | 128 | 0.019 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=16 | 114 | 146 | 0.018 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=18 | 128 | 164 | 0.018 seconds | false |
P_nonterminate | foraging::foraging::stm_ref0::N=20 | 142 | 182 | 0.027 seconds | false |
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
P_min_terminate | foraging::foraging::stm_ref0::N=2 | 16 | 20 | 0.004 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=4 | 30 | 38 | 0.005 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=6 | 44 | 56 | 0.007 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=8 | 58 | 74 | 0.004 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.004 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=12 | 86 | 110 | 0.005 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=14 | 100 | 128 | 0.005 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=16 | 114 | 146 | 0.005 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=18 | 128 | 164 | 0.005 seconds | 0.0 |
P_min_terminate | foraging::foraging::stm_ref0::N=20 | 142 | 182 | 0.008 seconds | 0.0 |
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
P_max_terminate | foraging::foraging::stm_ref0::N=2 | 16 | 20 | 0.005 seconds | 0.75 |
P_max_terminate | foraging::foraging::stm_ref0::N=4 | 30 | 38 | 0.008 seconds | 0.9375 |
P_max_terminate | foraging::foraging::stm_ref0::N=6 | 44 | 56 | 0.012 seconds | 0.984375 |
P_max_terminate | foraging::foraging::stm_ref0::N=8 | 58 | 74 | 0.013 seconds | 0.99609375 |
P_max_terminate | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.015 seconds | 0.9990234375 |
P_max_terminate | foraging::foraging::stm_ref0::N=12 | 86 | 110 | 0.018 seconds | 0.999755859375 |
P_max_terminate | foraging::foraging::stm_ref0::N=14 | 100 | 128 | 0.017 seconds | 0.99993896484375 |
P_max_terminate | foraging::foraging::stm_ref0::N=16 | 114 | 146 | 0.021 seconds | 0.9999847412109375 |
P_max_terminate | foraging::foraging::stm_ref0::N=18 | 128 | 164 | 0.022 seconds | 0.9999961853027344 |
P_max_terminate | foraging::foraging::stm_ref0::N=20 | 142 | 182 | 0.031 seconds | 0.9999980926513672 |
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
R_min_stop | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.012 seconds | Infinity |
Assertion | Const | States | Transitions | Time | Result |
---|---|---|---|---|---|
R_max_stop | foraging::foraging::stm_ref0::N=10 | 72 | 92 | 0.005 seconds | Infinity |
The P_max_terminate
result is also shown in the diagram below.
This example shows how to use RoboChart to model and verify probabilistic behaviour of a simple device using RoboTool.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements