Towards Industrial Formal Specification of Programmable Safety Systems

Formal methods for specification and verification are promising in developing PLC (Programmable Logic Controller) programs in manufacturing industry. Particularly this holds for safety PLCs, used to protect humans and equipment from injuries and damages. An important challenge though, is the development of formal specifications, typically a tough task for control engineers. This paper proposes a systematic work procedure that can be used as a first step of developing formal specifications of safety PLC programs in industry. The work procedure intends to facilitate the development of relevant formal properties for safety PLC program components. The formal specifications can be used for automatic formal verification of the components, using model checking techniques. The paper shows how the work procedure has been applied to industrial safety components, resulting in relevant and nontrivial specifications