Tell a friend
Print
Glück, Roland and Krebs, Florian (2015) Towards Interactive Verification of PLC Programs using MKA and KIV. In: 15th Int. Conf. on Relational and Algebraic Methods in Computer Science, 9348, pp. 241-256. Springer. 15th International Conference on Relational and Algebraic Methods in Computer Science, 28. Sep. - 01. Okt. 2015, Braga, Portugal. doi: 10.1007/978-3-319-24704-5. ISBN 978-3-319-24703-8.
![[img]](https://elib.dlr.de/style/images/fileicons/application_pdf.png) |
PDF (Vortragsfolien der Konferenz RAMiCS 2015)
1MB |
Official URL: http://www.springer.com/us/book/9783319247038
Abstract
In this paper we develop an approach to interactive verification of programmable logic controllers which often serve as controllers in safety critical systems and hence need thorough verification. As a verification tool we use the KIV system, whereas the formalization is done in modal Kleene algebra. We first prove a bunch of theorems from modal Kleene algebra in KIV, subsequently translate the desired properties of a program for a programmable logic controller in modal Kleene algebra, and finally prove these encoded properties interactively with KIV.
| Item URL in elib: | https://elib.dlr.de/98499/ | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Document Type: | Conference or Workshop Item (Speech) | ||||||||||||
| Title: | Towards Interactive Verification of PLC Programs using MKA and KIV | ||||||||||||
| Authors: |
| ||||||||||||
| Date: | September 2015 | ||||||||||||
| Journal or Publication Title: | 15th Int. Conf. on Relational and Algebraic Methods in Computer Science | ||||||||||||
| Refereed publication: | Yes | ||||||||||||
| Open Access: | Yes | ||||||||||||
| Gold Open Access: | No | ||||||||||||
| In SCOPUS: | No | ||||||||||||
| In ISI Web of Science: | No | ||||||||||||
| Volume: | 9348 | ||||||||||||
| DOI: | 10.1007/978-3-319-24704-5 | ||||||||||||
| Page Range: | pp. 241-256 | ||||||||||||
| Editors: |
| ||||||||||||
| Publisher: | Springer | ||||||||||||
| Series Name: | Lecture Notes in Computer Science | ||||||||||||
| ISBN: | 978-3-319-24703-8 | ||||||||||||
| Status: | Published | ||||||||||||
| Keywords: | Programmable Logic Controllers, KIV, Kleene Algebra, Interactive Verification, Temporal Logic | ||||||||||||
| Event Title: | 15th International Conference on Relational and Algebraic Methods in Computer Science | ||||||||||||
| Event Location: | Braga, Portugal | ||||||||||||
| Event Type: | international Conference | ||||||||||||
| Event Dates: | 28. Sep. - 01. Okt. 2015 | ||||||||||||
| Organizer: | HASLAB/Universidade do Minho | ||||||||||||
| HGF - Research field: | Aeronautics, Space and Transport | ||||||||||||
| HGF - Program: | Space | ||||||||||||
| HGF - Program Themes: | Space System Technology | ||||||||||||
| DLR - Research area: | Raumfahrt | ||||||||||||
| DLR - Program: | R SY - Space System Technology | ||||||||||||
| DLR - Research theme (Project): | R - Vorhaben Weiterentwicklung Robotik - Mechatronik und Dynamik (old) | ||||||||||||
| Location: | Augsburg | ||||||||||||
| Institutes and Institutions: | Institute of Structures and Design > Automation and Quality Assurance in Production | ||||||||||||
| Deposited By: | Glück, Dr. Roland | ||||||||||||
| Deposited On: | 19 Nov 2015 13:46 | ||||||||||||
| Last Modified: | 31 Jul 2019 19:55 |
Repository Staff Only: item control page
