Name
Abstract | ||
|---|---|---|
We give timed automaton models for a class of Pro- grammable Logic Controller (PLC) applications, that are programmed in a simple fragment of the language Instruc- tion Lists as defined in the standard IEC 1131-3. Two dif- ferent approaches for modelling timers are suggested, that lead to two different timed automaton models. The purpose of this work is to provide a basis for verificationand testing of real-time properties of PLC applications. Our work can be seen in broader context: it is a contributionto methodi- cal development of provably correct programs. Even if the present PLC hardware will be substituted by e.g. Personal Computers,withasimilaroperationmode, thedevelopment and verification method will remain useful. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1109/EMRTS.1999.777456 | ECRTS |
Keywords | Field | DocType |
automata theory,formal verification,programmable controllers,real-time systems,Instruction Lists,PLC,Programmable Logic Controller,provably correct programs,testing,timed automaton models,verification | Complex programmable logic device,Computer science,Simple programmable logic device,Programmable logic array,Real-time computing,Timed automaton,Programmable logic controller,Function block diagram,Formal verification,Programmable logic device | Conference |
ISSN | ISBN | Citations |
1068-3070 | 0-7695-0240-7 | 28 |
PageRank | References | Authors |
3.59 | 16 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Angelika Mader | 1 | 199 | 19.44 |
| H. Wupper | 2 | 29 | 4.68 |