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...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| 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!
|
| _version_ | 1832562241842446336 |
|---|---|
| author | Jie Zhang Yuntao Peng William N. N. Hung Xiaojuan Li Jindong Tan Zhiping Shi |
| author_facet | Jie Zhang Yuntao Peng William N. N. Hung Xiaojuan Li Jindong Tan Zhiping Shi |
| author_sort | Jie Zhang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-1921cddefd2f40e49462efa8ad6be529 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-1921cddefd2f40e49462efa8ad6be5292025-02-03T01:23:06ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/327465327465A Case Study on Formal Analysis of an Automated Guided Vehicle SystemJie Zhang0Yuntao Peng1William N. N. Hung2Xiaojuan Li3Jindong Tan4Zhiping Shi5College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, ChinaCollege of Information Science and Technology, Beijing University of Chemical Technology, Beijing, ChinaSynopsys Inc., Mountain View, CA, USABeijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, ChinaUniversity of Tennessee, Knoxville, TN, USABeijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, ChinaThis 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.http://dx.doi.org/10.1155/2014/327465 |
| spellingShingle | Jie Zhang Yuntao Peng William N. N. Hung Xiaojuan Li Jindong Tan Zhiping Shi A Case Study on Formal Analysis of an Automated Guided Vehicle System Journal of Applied Mathematics |
| title | A Case Study on Formal Analysis of an Automated Guided Vehicle System |
| title_full | A Case Study on Formal Analysis of an Automated Guided Vehicle System |
| title_fullStr | A Case Study on Formal Analysis of an Automated Guided Vehicle System |
| title_full_unstemmed | A Case Study on Formal Analysis of an Automated Guided Vehicle System |
| title_short | A Case Study on Formal Analysis of an Automated Guided Vehicle System |
| title_sort | case study on formal analysis of an automated guided vehicle system |
| url | http://dx.doi.org/10.1155/2014/327465 |
| work_keys_str_mv | AT jiezhang acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT yuntaopeng acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT williamnnhung acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT xiaojuanli acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT jindongtan acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT zhipingshi acasestudyonformalanalysisofanautomatedguidedvehiclesystem AT jiezhang casestudyonformalanalysisofanautomatedguidedvehiclesystem AT yuntaopeng casestudyonformalanalysisofanautomatedguidedvehiclesystem AT williamnnhung casestudyonformalanalysisofanautomatedguidedvehiclesystem AT xiaojuanli casestudyonformalanalysisofanautomatedguidedvehiclesystem AT jindongtan casestudyonformalanalysisofanautomatedguidedvehiclesystem AT zhipingshi casestudyonformalanalysisofanautomatedguidedvehiclesystem |