elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Impressum | Datenschutz | Kontakt | English
Schriftgröße: [-] Text [+]

Towards Interactive Verification of PLC Programs using MKA and KIV

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, 2015-09-28 - 2015-10-01, Braga, Portugal. doi: 10.1007/978-3-319-24704-5_15. ISBN 978-3-319-24703-8.

[img] 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:
AutorenInstitution oder E-Mail-AdresseAutoren-ORCID-iDORCID Put Code
Glück, Rolandroland.glueck (at) dlr.deNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Krebs, Florianflorian.krebs (at) dlr.dehttps://orcid.org/0000-0001-6033-801XNICHT SPEZIFIZIERT
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:
HerausgeberInstitution und/oder E-Mail-Adresse der HerausgeberHerausgeber-ORCID-iDORCID Put Code
Kahl, Wolframkahl (at) cas.mcmaster.caNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Winter, Michaelmwinter (at) brocku.caNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Oliveira, Joséjno (at) di.uminho.ptNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
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
Veranstaltungsbeginn:28 September 2015
Veranstaltungsende:1 Oktober 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:24 Apr 2024 20:03

Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags

Blättern
Suchen
Hilfe & Kontakt
Informationen
electronic library verwendet EPrints 3.3.12
Gestaltung Webseite und Datenbank: Copyright © Deutsches Zentrum für Luft- und Raumfahrt (DLR). Alle Rechte vorbehalten.