A tool for the certification of sequential function chart based system specifications

Blech, J 2011, 'A tool for the certification of sequential function chart based system specifications', in Jorg Brauer, Marco Roveri, Hendrik Tews (ed.) Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011), Nijmegen, Netherlands, 26 August 2011, pp. 81-96.


Document type: Conference Paper
Collection: Conference Papers

Title A tool for the certification of sequential function chart based system specifications
Author(s) Blech, J
Year 2011
Conference name SSV 2011
Conference location Nijmegen, Netherlands
Conference dates 26 August 2011
Proceedings title Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)
Editor(s) Jorg Brauer, Marco Roveri, Hendrik Tews
Publisher Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Place of publication Wadern, Germany
Start page 81
End page 96
Total pages 16
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.
Subjects Software Engineering
Copyright notice © 2011 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
ISBN 9783939897361
Versions
Version Filter Type
Access Statistics: 148 Abstract Views  -  Detailed Statistics
Created: Wed, 17 Jul 2013, 15:02:00 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us