Modeling, Specification and Construction of PLC-programs

• Main Authors: E. V. Kuzmin, V. A. Sokolov
• Format: Article
• Language: English
• Published: Yaroslavl State University 2013-04-01
• Series: Modelirovanie i Analiz Informacionnyh Sistem
• Subjects: programmable pogic controllers; software engineering; modeling and specification of plc-programs
• Online Access: https://www.mais-journal.ru/jour/article/view/209

A new approach to construction of reliable discrete PLC-programs with timers — programming based on specification and verification — is proposed. Timers are modelled in a discrete way. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to a LTLspecification. A new approach to programming of PLC is shown by an example. The proposed programming approach provides an ability of a correctness analysis of PLC-programs using the model checking method. The programming requires fulfillment of the following two conditions: 1) a value of each variable should be changed not more than once per one full PLC-program implementation (per one full working cycle of PLC); 2) a value of each variable should only be changed in one place of a PLC-program. Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable.