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

Jie Zhang; Yuntao Peng; William N. N. Hung; Xiaojuan Li; Jindong Tan; Zhiping Shi

doi:10.1155/2014/327465

Journal of Applied Mathematics (Jan 2014)

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

Jie Zhang,
Yuntao Peng,
William N. N. Hung,
Xiaojuan Li,
Jindong Tan,
Zhiping Shi

Affiliations

Jie Zhang: College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, China
Yuntao Peng: College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, China
William N. N. Hung: Synopsys Inc., Mountain View, CA, USA
Xiaojuan Li: Beijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, China
Jindong Tan: University of Tennessee, Knoxville, TN, USA
Zhiping Shi: Beijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, China

DOI: https://doi.org/10.1155/2014/327465
Journal volume & issue: Vol. 2014

Abstract

Read online

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.

Published in Journal of Applied Mathematics

ISSN: 1110-757X (Print); 1687-0042 (Online)
Publisher: Wiley
Country of publisher: United Kingdom
LCC subjects: Science: Mathematics
Website: https://onlinelibrary.wiley.com/journal/4185

About the journal