Verification Condition Generator for Revised Reflex Language Using Isabelle/HOL

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.