Versenden
Drucken
Glück, Roland und 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, Seiten 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_15. ISBN 978-3-319-24703-8.
![[img]](https://elib.dlr.de/style/images/fileicons/application_pdf.png) |
PDF (Vortragsfolien der Konferenz RAMiCS 2015)
1MB |
Offizielle URL: http://www.springer.com/us/book/9783319247038
Kurzfassung
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.
| elib-URL des Eintrags: | https://elib.dlr.de/98499/ | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Dokumentart: | Konferenzbeitrag (Vortrag) | ||||||||||||||||
| Titel: | Towards Interactive Verification of PLC Programs using MKA and KIV | ||||||||||||||||
| Autoren: |
| ||||||||||||||||
| Datum: | September 2015 | ||||||||||||||||
| Erschienen in: | 15th Int. Conf. on Relational and Algebraic Methods in Computer Science | ||||||||||||||||
| Referierte Publikation: | Ja | ||||||||||||||||
| Open Access: | Ja | ||||||||||||||||
| Gold Open Access: | Nein | ||||||||||||||||
| In SCOPUS: | Nein | ||||||||||||||||
| In ISI Web of Science: | Nein | ||||||||||||||||
| Band: | 9348 | ||||||||||||||||
| DOI: | 10.1007/978-3-319-24704-5_15 | ||||||||||||||||
| Seitenbereich: | Seiten 241-256 | ||||||||||||||||
| Herausgeber: |
| ||||||||||||||||
| Verlag: | Springer | ||||||||||||||||
| Name der Reihe: | Lecture Notes in Computer Science | ||||||||||||||||
| ISBN: | 978-3-319-24703-8 | ||||||||||||||||
| Status: | veröffentlicht | ||||||||||||||||
| Stichwörter: | Programmable Logic Controllers, KIV, Kleene Algebra, Interactive Verification, Temporal Logic | ||||||||||||||||
| Veranstaltungstitel: | 15th International Conference on Relational and Algebraic Methods in Computer Science | ||||||||||||||||
| Veranstaltungsort: | Braga, Portugal | ||||||||||||||||
| Veranstaltungsart: | internationale Konferenz | ||||||||||||||||
| Veranstaltungsdatum: | 28. Sep. - 01. Okt. 2015 | ||||||||||||||||
| Veranstalter : | HASLAB/Universidade do Minho | ||||||||||||||||
| HGF - Forschungsbereich: | Luftfahrt, Raumfahrt und Verkehr | ||||||||||||||||
| HGF - Programm: | Raumfahrt | ||||||||||||||||
| HGF - Programmthema: | Technik für Raumfahrtsysteme | ||||||||||||||||
| DLR - Schwerpunkt: | Raumfahrt | ||||||||||||||||
| DLR - Forschungsgebiet: | R SY - Technik für Raumfahrtsysteme | ||||||||||||||||
| DLR - Teilgebiet (Projekt, Vorhaben): | R - Vorhaben Weiterentwicklung Robotik - Mechatronik und Dynamik (alt) | ||||||||||||||||
| Standort: | Augsburg | ||||||||||||||||
| Institute & Einrichtungen: | Institut für Bauweisen und Strukturtechnologie > Automatisierung und Qualitätssicherung in der Produktionstechnologie | ||||||||||||||||
| Hinterlegt von: | Glück, Dr. Roland | ||||||||||||||||
| Hinterlegt am: | 19 Nov 2015 13:46 | ||||||||||||||||
| Letzte Änderung: | 11 Jul 2023 12:04 |
Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags
