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

Towards Interactive Verification of Programmable Logic Controllers using Modal Kleene Algebra and KIV

Glück, Roland and Krebs, Florian (2015) Towards Interactive Verification of Programmable Logic Controllers using Modal Kleene Algebra and KIV. Lecture Notes in Computer Science, 9348, pp. 241-256. Springer. DOI: 10.1007/978-3-319-24704-5 ISBN 978-3-319-24703-8 ISSN 0302-9743

Full text not available from this repository.

Official URL: http://link.springer.com/chapter/10.1007%2F978-3-319-24704-5_15

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/98498/
Document Type:Article
Title:Towards Interactive Verification of Programmable Logic Controllers using Modal Kleene Algebra and KIV
Authors:
AuthorsInstitution or Email of AuthorsAuthors ORCID iD
Glück, Rolandroland.glueck (at) dlr.deUNSPECIFIED
Krebs, Florianflorian.krebs (at) dlr.deUNSPECIFIED
Date:2015
Journal or Publication Title:Lecture Notes in Computer Science
Refereed publication:Yes
Open Access:No
Gold Open Access:No
In SCOPUS:Yes
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
ISSN:0302-9743
ISBN:978-3-319-24703-8
Status:Published
Keywords:PLC, interactive verification, KIV, Kleene algebra, temporal logic
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 10:54
Last Modified:06 Sep 2019 15:22

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.