Mathematical analysis of stage-based programmable logic controller
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. (C) 2011 Elsevier Ltd. All rights reserved.
programmable logic controller stage suspended boom extended duration calculus