Formal Verification of Real-Time Function Blocks Using PVS

Linna Pang
(McMaster University)
Chen-Wei Wang
(McMaster University)
Mark Lawford
(McMaster University)
Alan Wassyng
(McMaster University)
Josh Newell
(Systemware Innovation Corporation)
Vera Chow
(Systemware Innovation Corporation)
David Tremaine
(Systemware Innovation Corporation)

A critical step towards certifying safety-critical systems is to check their conformance to hard real-time requirements. A promising way to achieve this is by building the systems from pre-verified components and verifying their correctness in a compositional manner. We previously reported a formal approach to verifying function blocks (FBs) using tabular expressions and the PVS proof assistant. By applying our approach to the IEC 61131-3 standard of Programmable Logic Controllers (PLCs), we constructed a repository of precise specification and reusable (proven) theorems of feasibility and correctness for FBs. However, we previously did not apply our approach to verify FBs against timing requirements, since IEC 61131-3 does not define composite FBs built from timers. In this paper, based on our experience in the nuclear domain, we conduct two realistic case studies, consisting of the software requirements and the proposed FB implementations for two subsystems of an industrial control system. The implementations are built from IEC 61131-3 FBs, including the on-delay timer. We find issues during the verification process and suggest solutions.

In Jun Pang, Yang Liu and Sjouke Mauw: Proceedings 4th International Workshop on Engineering Safety and Security Systems (ESSS 2015), Oslo, Norway, June 22, 2015, Electronic Proceedings in Theoretical Computer Science 184, pp. 65–79.
Published: 10th June 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.184.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org