Beitrag in einem Tagungsband
Design of verified logic control programs
Details zur Publikation
Autor(inn)en: | Lohmann, S.; Dinh Thi, L.; Stursberg, O. |
Herausgeber: | IEEE |
Publikationsjahr: | 2006 |
Seitenbereich: | 1855-1860 |
Buchtitel: | Computer Aided Control System Design, 2006 IEEE International Conference on Control Applications, 2006 IEEE International Symposium on Intelligent Control, 2006 IEEE |
ISBN: | 0-7803-9797-5 |
DOI-Link der Erstveröffentlichung: |
Zusammenfassung, Abstract
To complement the largely manual design of logic control programs in industrial practice, this contribution proposes a method for systematically (and partly algorithmically) deriving logic controllers for given specifications. The main idea is to structure the information available for the design in form of specific intermediate formats which are iteratively refined and straightforwardly lead to controllers formulated as Sequential Function Charts. To analyze whether the design complies with all given specifications, model-based verification is applied subsequently, i.e. the controller is converted into timed automata, the latter are composed with a plant model, and model-checking algorithmically verifies (or falsifies) logic properties for the composed system. The procedure is described here for the example of a multi-product batch plant.
To complement the largely manual design of logic control programs in industrial practice, this contribution proposes a method for systematically (and partly algorithmically) deriving logic controllers for given specifications. The main idea is to structure the information available for the design in form of specific intermediate formats which are iteratively refined and straightforwardly lead to controllers formulated as Sequential Function Charts. To analyze whether the design complies with all given specifications, model-based verification is applied subsequently, i.e. the controller is converted into timed automata, the latter are composed with a plant model, and model-checking algorithmically verifies (or falsifies) logic properties for the composed system. The procedure is described here for the example of a multi-product batch plant.
