PLC-Automata: A New Class of Implementable Real-Time Automata

We introduce PLC-Automata as a new class of automata which are tailored to deal with real-time properties of Programmable Logic Controllers (PLCs). These devices are often used in industrial practice to solve controlling problems. Nevertheless, PLC-Automata are not restricted to PLCs, but can be seen as a model for all polling systems. A semantics in an appropriate real-time temporal logic (Duration Calculus) is given and an implementation schema that ts the semantics is presented in a programming language for PLCs. A case study is used to demonstrate the suitability of this approach. We de ne several parallel composition operators, and present an alternative semantics in terms of Timed Automata for which modelcheckers are available. Key words: Real-time, Speci cation, Formal Methods, Duration Calculus, PLC

• Type: Conference
• Year: 1997
• Where: ARTS
• Authors: Henning Dierks
• Keywords: ARTS 1997, ARTS 1999, Duration Calculus, Programmable Logic Controllers, Real-time Temporal Logic