A Case Study on Formal Analysis of an Automated Guided Vehicle System

This paper considers a hybrid I/O automata model for an automated guided vehicle (AGV) system. A set of key properties of an AGV system are characterized for the correctness of the system. An abstract model is constructed from the hybrid automata model to simplify the proof of the constraints. The t...

Full description

Saved in:
Bibliographic Details
Main Authors: Jie Zhang, Yuntao Peng, William N. N. Hung, Xiaojuan Li, Jindong Tan, Zhiping Shi
Format: Article
Language:English
Published: Wiley 2014-01-01
Series:Journal of Applied Mathematics
Online Access:http://dx.doi.org/10.1155/2014/327465
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper considers a hybrid I/O automata model for an automated guided vehicle (AGV) system. A set of key properties of an AGV system are characterized for the correctness of the system. An abstract model is constructed from the hybrid automata model to simplify the proof of the constraints. The two models are equivalent in terms of bisimulation relation. We derive the constraints to ensure the correctness of the properties. We validate the system by analyzing the parameters of the constraints of the AGV system.
ISSN:1110-757X
1687-0042