Formal Verification of Real-Time Function Blocks Using PVS

TL;DR

This paper extends formal verification of function blocks in IEC 61131-3 to include timing requirements, using PVS, demonstrated through two industrial control system case studies.

Contribution

It applies PVS-based formal verification to verify timing constraints of IEC 61131-3 function blocks, including timers, in realistic industrial scenarios.

Findings

Identified issues in verifying timing constraints of FBs

Proposed solutions for timing verification challenges

Validated approach on two industrial control system subsystems

Abstract

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.