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...

Full description

Saved in:
Bibliographic Details
Main Authors: Anping He, Jinzhao Wu, Shihan Yang, Yongquan Zhou, Juan Wang
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