elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

Towards Interactive Verification of PLC Programs using MKA and KIV

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] 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:
AuthorsInstitution or Email of AuthorsAuthors ORCID iD
Glück, Rolandroland.glueck (at) dlr.deUNSPECIFIED
Krebs, Florianflorian.krebs (at) dlr.deUNSPECIFIED
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:
EditorsEmail
Kahl, Wolframkahl@cas.mcmaster.ca
Winter, Michaelmwinter@brocku.ca
Oliveira, Joséjno@di.uminho.pt
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 Technology
DLR - Research area:Raumfahrt
DLR - Program:R SY - Technik für Raumfahrtsysteme
DLR - Research theme (Project):R - Vorhaben Weiterentwicklung Robotik - Mechatronik und Dynamik
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

Browse
Search
Help & Contact
Information
electronic library is running on EPrints 3.3.12
Copyright © 2008-2017 German Aerospace Center (DLR). All rights reserved.