Abstract
We describe a tool framework for certifying properties of sequential function chart (SFC)based system specifications: CertPLC. CertPLC handles programmable logic controller (PLC) descriptions provided in the SFC language of the IEC 61131–3 standard. It provides routines to
certify properties of systems by delivering an independently checkable formal system description and proof (called certificate) for the desired properties. We focus on properties that can be
described as inductive invariants. System descriptions and certificates are generated and handled using the Coq proof assistant. Our tool framework is used to provide supporting evidence for the safety of embedded systems in the industrial automation domain to third-party authorities. In this paper we focus on the tool's architecture, requirements and implementation aspects.
BibTeX - Entry
@InProceedings{blech:OASIcs:2012:3590,
author = {Jan Olaf Blech},
title = {{A Tool for the Certification of Sequential Function Chart based System Specifications}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {57--70},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {J{\"o}rg Brauer and Marco Roveri and Hendrik Tews},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3590},
URN = {urn:nbn:de:0030-drops-35904},
doi = {10.4230/OASIcs.SSV.2011.57},
annote = {Keywords: Software/Program Verification}
}
|
Keywords: |
|
Software/Program Verification |
|
Collection: |
|
6th International Workshop on Systems Software Verification |
|
Issue Date: |
|
2012 |
|
Date of publication: |
|
13.07.2012 |
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)