salle A. Turing CE4
9 February 2012 - 14h00
Proof Assistant Based Certification for Modeling Languages and its Application to PLC Development
by Jan Olaf Blech from Fortiss
Abstract: This talk gives an overview on our work on proof assistant based
certification of system models: We automatically generate system model
representations for Coq out of Eclipse based modeling tools and
provide support for verification work on this. The focus of the talk
is on work for Programmable Logic Controllers (PLC). PLC are widely
used in embedded systems for the industrial automation domain and are
frequently programmed using languages from the IEC 61131--3 standard.
We have formalized parts of the IEC 61131--3 semantics in the proof
assistant Coq. We automatically generate parts of the Coq
representations of graphical IEC 61131--3 models and talk about their
usage for verification purposes. Finally, additional applications of
proof assistant based certification of modeling languages are
presented.
Jan Blech is a researcher in the Software & Systems Engineering group
at fortiss. His main research topics are in formal methods and
software engineering. Previously he was a PostDoc at Verimag and
completed a PhD in Germany. He has worked on several national (both
German and French) funded projects and led a workpackage in one EU
project at fortiss.
