Validating Programmable Logic Controller Systems with Duration Calculus
The Programmable Logic Controller (PLC) system is a type of the hybrid systems, which is a widely used safety-critical system in industry. It is regarded that the formal method is a valuable and indispensable way of analyzing and validating the PLC systems. However, which formal methods and how to use the methods are challenges. In this paper, the authors propose a specific formal method of the PLC systems, e.g., they formalize the PLC systems by the EDC formulae hierarchically, specify the property as the formulae and then analyze and verify the system in the framework of the EDC calculus.