Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model

Abstract

Ensuring the reliability of embedded systems has become very important. Reliability may be ensured by a number of formal verification techniques including model checking. We study one such verification technique through a physical example of an embedded system, a line tracing robot. This paper describes how to model the behavior of a line tracing robot program as a network of timed automata and we also present experimental results for this verification by the UPPAAL model checker. The line tracer was built us- ing LEGO Mindstorms and this paper also describes the im- plementation using LeJOS, a Java development environment for LEGO Mindstorms.