DROPS

Document

DOI: 10.4230/OASIcs.SSV.2011.57

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

Authors: Jan Olaf Blech

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

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.

Cite as

Jan Olaf Blech. A Tool for the Certification of Sequential Function Chart based System Specifications. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 57-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{blech:OASIcs.SSV.2011.57,
  author =	{Blech, Jan Olaf},
  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 =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.57},
  URN =		{urn:nbn:de:0030-drops-35904},
  doi =		{10.4230/OASIcs.SSV.2011.57},
  annote =	{Keywords: Software/Program Verification}
}

Search Results

Documents authored by Blech, Jan Olaf

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

Abstract

Cite as

Thanks for your feedback!

Could not send message