English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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. Keywords-component; verification; model checking; line tracing robot; 2-dimensional geometric modeling

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