License
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.57
URN: urn:nbn:de:0030-drops-35904
URL: http://drops.dagstuhl.de/opus/volltexte/2012/3590/
Go to the corresponding OASIcs Volume Portal


Blech, Jan Olaf

A Tool for the Certification of Sequential Function Chart based System Specifications

pdf-format:
Document 1.pdf (352 KB)


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 611313 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 =		{http://dx.doi.org/10.4230/OASIcs.SSV.2011.57},
  annote =	{Keywords: Software/Program Verification}
}

Keywords: Software/Program Verification
Seminar: 6th International Workshop on Systems Software Verification
Issue Date: 2012
Date of publication: 12.07.2012


DROPS-Home | Fulltext Search | Imprint Published by LZI