Towards Interactive Verification of Programmable Logic Controllers using Modal Kleene Algebra and KIV

Abstract

This talk introduces an approach to interactive verification of programmable logic controllers which often serve as controllers in safety critical systems and hence need thorough verification. It gives first a short introduction to programmable logic controllers, afterwards an introduction to the framework of modal Kleene Algebra and a short view of the interactive proving system KIV. Finally, it is shown how Kleene Algebra can be used to verify LTL properties of programmable logic controllers using the KIV system.