概要: Recently reliability of embedded systems has become very important. Such reliability can be ensured by formal verification techniques including model checking. We study such verification technique through a real example of embedded systems, a line tracer. This paper mainly describes how to model the behavior of the line tracer in a network of timed automata, as well as experimental results of verification. Using the model, several safety properties are successfully verified with a model checker, UPPAAL. The line tracer is built with LEGO Mindstorms kit. This paper also describes the implementation using LeJOS, a Java development environment for LEGO Mindstorms kit. タグ: automaton, line, model, program, property, safety, timed, tracer, verification

@inproceedings{KozoOkano2012,
  author = {Kozo Okano and Toshifusa Sekizawa and Hiroaki Shimba and Hideki Kawai and Kentaro Hanada and Yukihiro Sasaki and Shinji Kusumoto},
  title = {Verification of Safety Property of Line Tracer Program using Timed Automaton Model},
  booktitle = {International Workshop on Informatics 2012},
  pages = {136--142},
  year = {2012},
  month = {sep}
}