
On Construction and Verification of PLC-Programs
Author(s) -
E. V. Kuzmin,
Valery A. Sokolov
Publication year - 2015
Publication title -
modelirovanie i analiz informacionnyh sistem
Language(s) - English
Resource type - Journals
eISSN - 2313-5417
pISSN - 1818-1015
DOI - 10.18255/1818-1015-2012-4-25-36
Subject(s) - correctness , programming language , computer science , lock (firearm) , model checking , programmable logic controller , code (set theory) , usability , program code , logic programming , embedded system , operating system , engineering , mechanical engineering , set (abstract data type)
We review some methods and approaches to programming discrete problems for Programmable Logic Controllers on the example of constructing PLC-programs for controling a code lock. For these approaches we evaluate the usability of the model checking method for the analysis of program correctness with respect to the automatic verification tool Cadence SMV. Some possible PLC-program vulnerabilities arising at a number approaches to programming of PLC are revealed.