English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

A critical step towards certifying safety-critical systems is to check theirconformance to hard real-time requirements. A promising way to achieve this isby building the systems from pre-verified components and verifying theircorrectness in a compositional manner. We previously reported a formal approachto verifying function blocks (FBs) using tabular expressions and the PVS proofassistant. By applying our approach to the IEC 61131-3 standard of ProgrammableLogic Controllers (PLCs), we constructed a repository of precise specificationand reusable (proven) theorems of feasibility and correctness for FBs. However,we previously did not apply our approach to verify FBs against timingrequirements, since IEC 61131-3 does not define composite FBs built fromtimers. In this paper, based on our experience in the nuclear domain, weconduct two realistic case studies, consisting of the software requirements andthe proposed FB implementations for two subsystems of an industrial controlsystem. The implementations are built from IEC 61131-3 FBs, including theon-delay timer. We find issues during the verification process and suggestsolutions.

Formal Verification of Real-Time Function Blocks Using PVS