Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects
Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, Shinji Kusumoto · 2014
The demand for embedded systems have increased in our society. Ensuring the safety properties of these systems has also become important. Model checking is a technique to ensure such systems. Our target is formal verification of hybrid systems which contain both continuous and discrete behaviors. For the goal, we have studied properties of a line tracing robot built using LEGO Mindstorms with a control program written in LeJOS. We have already presented verification of safety properties of a control program for the application using model checker UPPAAL. In the previous study, we were in a preliminary stage and set limitations. In this presentation, we extend our previous study. In general, a real course can be expressed in combinations of straight and arc courses. First, we verify properties of the same control program for arc courses. Next, in case of the line tracer can not keep track, we analyze turning angle using counter examples. Above-mentioned two approaches are necessary from the standpoint of design phase.