Applying REMES behavioral modeling to PLC systems

Abstract—Programmable logic controllers (PLCs), as aspecialized type of embedded systems, have been introduced toincrease system flexibility and reliability, but at the same time togive faster response time and lower cost of implementation. Inthe beginning, their use brought a revolutionary change, but withthe constant growth of system complexity, it became harder toguarantee both functional and extra functional properties, asearly as possible in the development process. In this paper, weshow how formal methods can be applied to describe PLC-basedsystems and illustrate it on an example of a car wash system.First, we show how the existing behavioral modeling languageREMES (REsource Model for Embedded Systems) can beextended to model the behavior of such systems. Second, we showhow REMES can be translated into networks of timed automataand priced timed automata in order to support safety andresource-wise reasoning about PLC systems. The formalverification of PLC systems is carried out in the UPPAAL andUPPAAL CORA tools.ProgressQ-Impres