License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.57
URN: urn:nbn:de:0030-drops-35904
Go to the corresponding OASIcs Volume Portal

Blech, Jan Olaf

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

6.pdf (0.3 MB)


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

  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 =		{},
  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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI