Automata-Based Analysis of Stage Suspended Boom Systems
A stage suspended boom system is an automatic steeve system orchestrated by the PLC (programmable logic controller). Security and fault-recovering are two important properties. In this paper, we analyze and verify the boom system formally. We adopt the hybrid automaton to model the boom system. The...
Saved in:
Main Authors: | , , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Wiley
2013-01-01
|
Series: | Journal of Applied Mathematics |
Online Access: | http://dx.doi.org/10.1155/2013/739253 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
_version_ | 1832556751448178688 |
---|---|
author | Anping He Jinzhao Wu Shihan Yang Yongquan Zhou Juan Wang |
author_facet | Anping He Jinzhao Wu Shihan Yang Yongquan Zhou Juan Wang |
author_sort | Anping He |
collection | DOAJ |
description | A stage suspended boom system is an automatic steeve system orchestrated by the PLC (programmable logic controller). Security and fault-recovering are two important properties. In this paper, we analyze and verify the boom system formally. We adopt the hybrid automaton to model the boom system. The forward reachability is used to verify the properties with the reachable states. We also present a case study to illustrate the feasibility of the proposed verification. |
format | Article |
id | doaj-art-7aa0e987724c400d8dffe7f1a9276e8b |
institution | Kabale University |
issn | 1110-757X 1687-0042 |
language | English |
publishDate | 2013-01-01 |
publisher | Wiley |
record_format | Article |
series | Journal of Applied Mathematics |
spelling | doaj-art-7aa0e987724c400d8dffe7f1a9276e8b2025-02-03T05:44:29ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/739253739253Automata-Based Analysis of Stage Suspended Boom SystemsAnping He0Jinzhao Wu1Shihan Yang2Yongquan Zhou3Juan Wang4Guangxi Key Lab of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, ChinaGuangxi Key Lab of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, ChinaGuangxi Key Lab of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, ChinaGuangxi Key Lab of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, ChinaSchool of Civil Engineering and Mechanics, Lanzhou University, Lanzhou 730000, ChinaA stage suspended boom system is an automatic steeve system orchestrated by the PLC (programmable logic controller). Security and fault-recovering are two important properties. In this paper, we analyze and verify the boom system formally. We adopt the hybrid automaton to model the boom system. The forward reachability is used to verify the properties with the reachable states. We also present a case study to illustrate the feasibility of the proposed verification.http://dx.doi.org/10.1155/2013/739253 |
spellingShingle | Anping He Jinzhao Wu Shihan Yang Yongquan Zhou Juan Wang Automata-Based Analysis of Stage Suspended Boom Systems Journal of Applied Mathematics |
title | Automata-Based Analysis of Stage Suspended Boom Systems |
title_full | Automata-Based Analysis of Stage Suspended Boom Systems |
title_fullStr | Automata-Based Analysis of Stage Suspended Boom Systems |
title_full_unstemmed | Automata-Based Analysis of Stage Suspended Boom Systems |
title_short | Automata-Based Analysis of Stage Suspended Boom Systems |
title_sort | automata based analysis of stage suspended boom systems |
url | http://dx.doi.org/10.1155/2013/739253 |
work_keys_str_mv | AT anpinghe automatabasedanalysisofstagesuspendedboomsystems AT jinzhaowu automatabasedanalysisofstagesuspendedboomsystems AT shihanyang automatabasedanalysisofstagesuspendedboomsystems AT yongquanzhou automatabasedanalysisofstagesuspendedboomsystems AT juanwang automatabasedanalysisofstagesuspendedboomsystems |