Copyright © 2013 Anping He et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
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.