Verificação automática de sistemas descritos usando a linguagem Ladder

Abstract

Programmable Logic Controllers (PLC) were introduced in the 1960s to support modernization and maintenance of control, sequencing and interlocking logic of industrial plants and, since then, they became indispensable in industrial automation and control. A PLC is a digital computer built to operate in harsh industrial environments and designed to be easily operated by maintenance teams. Hence, it offers a set of programming languages directed to these professionals. One of such languages is the Ladder Diagram (LD), which is based on relay logic and still is one of the most used PLC programming languages. Verifying PLC programs is imperative to guaranteeing the safe operation of industrial plants and several works have addressed this issue in the literature. However, available methods for verification of LD usually employs a naive modelling approach, not taking into account the execution order of the rungs, which are program lines in LD. Besides, most of them focus only on Boolean operations, which are a subset of the possible commands available in LD. This work addresses both these issues, providing a complete methodology for translating Ladder Diagrams to NuSMV, which is the formal language. We validated the methodology with respect to execution order using constructed examples and also built a tool to translate LD exported from a PLC suite largely used in industry to NuSMV.