Execution
Verification Results
There are eight modules described with the BIP language that are running in DALA. Their functions are (1) collecting data from the laser sensors (SICK), (2) generating an obstacle map (Aspect), (3) navigating using the near diagram approach (NDD), (4) managing the low level robot wheel controller (RFLEX), (5) emulating the communication with an orbiter (Antenna), (6) providing power and energy for the robot (Battery), (7) heating the robot in a low temperature environment (Heating) and (8) controlling the movement of two cameras (Platine). All together the embedded code of DALA contains more than 500 000 lines of C code. The topology of the modules and the description of the behaviors of the components are complex. This is beyond the scope of tools such as NuSMV or SPIN. We first checked deadlock properties of individual modules. Both global and FP fails to check for deadlock-freedom. However, by using Incr, we can always generate the invariants and check the deadlock-freedom of all the modules. Table below shows the time consumption in computing invariants for deadlock-freedom checking of seven modules by the incremental method; it also gives the number of states per module. In these modules we have successively detected (and corrected) two deadlocks within Antenna and NDD, respectively.
| Module | comp | inters | locs | b | int | dls | time (m:s) | mem (mb) |
|---|---|---|---|---|---|---|---|---|
| RFLEX | 56 | 227 | 308 | 30 | 16 | 0 | 9:39 | 165 |
| NDD | 27 | 117 | 152 | 16 | 10 | 0 | 14:25 | 113 |
| Sick | 43 | 202 | 213 | 18 | 10 | 0 | 6:07 | 92 |
| Aspect | 29 | 117 | 160 | 16 | 11 | 0 | 1:00 | 80 |
| Battery | 30 | 138 | 176 | 21 | 11 | 0 | 4:43 | 65 |
| Heating | 26 | 116 | 149 | 18 | 12 | 0 | 0:39 | 57 |
| Platine | 37 | 151 | 174 | 16 | 9 | 0 | 8:47 | 97 |
Aside from the deadlock-freedom requirement, some modules also have safety property requirements such as causality (a service can be triggered only after a certain service has been running successfully, i.e., only if the variable corresponding to this service is set to true). In checking the causality requirement between different services, we need to compute invariants according to different causality requirement. Inspired from the invariant preservation properties, we removed some tight synchronizations between some components that would not synchronize directly with the components involved in the property and obtained a module with looser synchronized interactions. As the invariant of the module with looser synchronizations is preserved by the one with tighter synchronizations, if a property is satisfied in the former, then it is satisfied in the latter. Based on this fact, we could obtain the satisfied causality property in 17 seconds, while it took 1003 seconds before using the preorder.
