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

Author Jan Olaf Blech

Thumbnail PDF


  • Filesize: 352 kB
  • 14 pages

Document Identifiers

Author Details

Jan Olaf Blech

Cite AsGet BibTex

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)


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.
  • Software/Program Verification


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads