| Synthesizing Controllers from Real-Time Specifications |
| Henning Dierks |
| 关键词：Controller synthesis, duration calculus, embedded systems, formal methods, formal verification, programmable logic controller (PLC), timing verification |
| 主要内容：We present an algorithm for synthesizing real-time controllers specified in a subset of the interval temporal logic duration calculus. The synthesized controllers are given in terms of programmable logic controller (PLC)-automata, which are an abstract description of programs of polling machines. PLCautomata can be implemented directly on PLC’s, a special kind of polling real-time controllers that are often used in industry to control production cells and batch processes. We prove the correctness of the algorithm by the duration calculus semantics for PLC-automata. Furthermore, the set of specifications on which the algorithm terminates with a well-formed PLC-automaton coincides with the set of specifications that are implementable in principle. Hence, the algorithm also decides whether a specification given in this subset of the duration calculus is implementable.We demonstrate the behavior of the algorithm by an example and apply the algorithm to the well-known “gasburner” case study... |
| 《1999 IEEE》 |
| 全文下载请进入http://hightech.stlib.cn/tpi_1/sysasp/include/index.asp |
微信公众号