Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
472934 | Computers & Mathematics with Applications | 2011 | 17 Pages |
Abstract
The modern stage suspended boom system is automatically controlled by PLC (programmable logic controller), and represents a typical hybrid behavior. It is an important family of stage control machinery systems. This paper presents a formal approach to modeling the system behaviors of different scenes. The system is formally characterized and specified in a timed model. System properties are proved in the proof system of the extended duration calculus. The case study illustrates the feasibility of the proposed verification framework.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computer Science (General)
Authors
Anping He, William N.N. Hung, Guowu Yang, Jinzhao Wu, Lian Li,