Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects

The demand for embedded systems have increased in our society. Ensuring the safety propertiesof these systems has also become important. Model checking is a technique to ensure such systems. Our target is formal verificationof 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 propertiesof 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.