TY - GEN

T1 - Verification Condition Generator for Revised Reflex Language Using Isabelle/HOL

AU - Ищенко, Артем Дмитриевич

AU - Ануреев, Игорь Сергеевич

N1 - Conference code: 26

PY - 2025/8/8

Y1 - 2025/8/8

N2 - Process-oriented programming is an approach to software development that emphasizes the management of control systems through abstractions of processes and their states. In the realm of industrial control systems, where safety is critical, the process-oriented language Reflex is a key programming tool. However, to ensure the reliability and safety of these systems, formal verification techniques must be used. One such technique is deductive verification, which involves formalizing programs and their requirements as logical formulas known as verification conditions. The proof of these conditions indicates the correctness of the program according to its requirements. The automatic generation of correctness conditions is done using a special software tool called verification condition generator. We already proposed a verification condition generator for an early version of the Reflex language; however, it was significantly changed to implement more complex operational logic. This article introduces a rework of an earlier developed generator adapted for existing changes in the Reflex language and utilizing the control-flow graph for inner program representation. The implemented changes also make it more flexible to use with different logical systems.

AB - Process-oriented programming is an approach to software development that emphasizes the management of control systems through abstractions of processes and their states. In the realm of industrial control systems, where safety is critical, the process-oriented language Reflex is a key programming tool. However, to ensure the reliability and safety of these systems, formal verification techniques must be used. One such technique is deductive verification, which involves formalizing programs and their requirements as logical formulas known as verification conditions. The proof of these conditions indicates the correctness of the program according to its requirements. The automatic generation of correctness conditions is done using a special software tool called verification condition generator. We already proposed a verification condition generator for an early version of the Reflex language; however, it was significantly changed to implement more complex operational logic. This article introduces a rework of an earlier developed generator adapted for existing changes in the Reflex language and utilizing the control-flow graph for inner program representation. The implemented changes also make it more flexible to use with different logical systems.

KW - Reflex

KW - verification condition generator

KW - deductive verification

KW - Isabelle/HOL

KW - process-oriented programming

KW - control-flow graph

UR - https://www.scopus.com/pages/publications/105014139802

U2 - 10.1109/EDM65517.2025.11096836

DO - 10.1109/EDM65517.2025.11096836

M3 - Conference contribution

SN - 9781665477376

T3 - International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM

SP - 1440

EP - 1445

BT - International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM

PB - IEEE Computer Society

T2 - 2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM)

Y2 - 27 June 2025 through 1 July 2025

ER -