2D Geometric Modeling and Verification of Line Tracing Robot Using UPPAAL Model Checker

DOI

10.2991/sekeie-14.2014.36How to use a DOI?

Keywords

Component; verification; model checking; line tracing robot; 2-dimensional geometric modeling

Abstract

Model checking is one of the formal methods for verification of hardware and software systems. A model checker verifies queries described in temporal logic formulas about a model defined as a state transition diagram. Since the model checkers make an exhaustive search of the state space, the key point is how to reduce the state space in order to avoid an explosion of the number of states. The UPPAAL model checker is a model checker based on Timed CTL which is suitable for handling real-time systems. A line tracing robot, a typical example of real-time embedded systems, is a small electric car with motors and photo-sensors that follows a line on the ground. In this paper, we study the methodology of modeling and verification of the line tracing robot. In particular, we focus on two-dimensional geometric modeling which is acceptable for model checking without leading to state explosion.

Copyright

© 2014, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Yuta Nakatani
AU  - Shin-ya Nishizaki
PY  - 2014/03
DA  - 2014/03
TI  - 2D Geometric Modeling and Verification of Line Tracing Robot Using UPPAAL Model Checker
BT  - Proceedings of the 2nd International Conference on Software Engineering, Knowledge Engineering and Information Engineering (SEKEIE 2014)
PB  - Atlantis Press
SP  - 150
EP  - 155
SN  - 1951-6851
UR  - https://doi.org/10.2991/sekeie-14.2014.36
DO  - 10.2991/sekeie-14.2014.36
ID  - Nakatani2014/03
ER  -