Dala Robot


 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.


Contact | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4193668