Formal analysis of stage suspended boom systems with Extended Duration Calculus

The stage suspended boom systems are widely used to achieve the imaginative shows, especially for stunts. The physical mechanism of this kind of boom system is always fixed, but the scene of shows is variable, which always controlled by PLC (Programable Logic Controller) automatically. So it is interesting to describe a common way of modeling the requirements of different scene, which should be easy validated. We propose EDC (Extended Duration Calculus) to formalize the specification and then verify the request, which shows this kind of modelling and verifying framework is adoptable and practical.