Control systems play a crucial role in various domains necessitating high reliability and proof of correct software operation. To address this, formal methods, such as deductive verification, are employed to ensure the correctness of safety-critical software mathematically. This process involves generating verification conditions from the program's axiomatic semantics and its requirements. Main disadvantage of manual verification condition generation is its labor-intensity and prone to human error, which leads to the development of automated verification condition generators. However, they produce excessive or overly complex verification conditions that do not accurately reflect the possible program's operational paths. To mitigate the second issue, domain-oriented languages like Reflex have been introduced, which adopt a process-oriented paradigm to streamline programming and simplify verification condition generation. Nevertheless, the inherent switch-case structure of Reflex can lead to an increase in the number of verification conditions, exacerbating the first issue and complicating the selection of relevant ones. This paper proposes a simple static analysis system designed to optimize the generation of verification conditions for Reflex programs, enhancing the efficiency of the verification process. It is based on attaching attributes to different statements. Then, throughout the verification condition generation these attributes are collected and checked to be compatible with previously collected. If attributes are incompatible then verification condition are discarded.

Process-oriented programming is an approach to the development of control software in which a program is defined as a set of interacting processes. PoST is a process-oriented language that extends ST language from the IEC 61131-3 standard. In the field of control software development, formal verification plays an important role because of the need to ensure the high reliability of such software. Deductive verification is a formal verification method in which a program and requirements for it are presented in the form of logical formulas and logical inference is used to prove that the program satisfies the requirements. Control software is often subject to temporal requirements. We formalize such requirements for process-oriented programs in the form of control loop invariants. But control loop invariants representing requirements are not sufficient for proving program correctness. Therefore, we add extra invariants that contain auxiliary information. This paper addresses the problem of automating deductive verification of process-oriented programs. We propose an approach in which temporal requirements are specified using requirement patterns that are constructed from basic patterns. For each requirement pattern the corresponding extra invariant pattern and lemmas are defined. The proposed approach allows us to make the deductive verification of process-oriented programs more automated.

In this paper, we formally describe real-time systems with an abstract scheduler using Kripke structures. This formalization allows us to refine the abstract scheduler in its terms. We illustrate this approach with a non-preemptive global fixed priority scheduler (NE-GFP). We also formulate a safety property for real time systems using linear temporal logic LTL. We implement our formalization of real-time systems with a NE-GFP scheduler in language Promela used in the SPIN verification tool and make experiments for proving or disproving the safety property to evaluate the effectiveness of our approach.

Reachability probabilities and expected rewards are two important classes of properties that are used in probabilistic model checking. Iterative numerical methods are applied to compute the underlying properties. To guarantee soundness of the computed results, the interval iteration method is used. This method utilizes two vectors as the upper-bound and lower-bound of values and uses the standard value iteration method to update the values of these vectors. In this paper, we use a combination of value iteration and policy iteration to update these values. We use policy iteration to update the values of the lower bound vector. For the upper-bound vector, we use a modified version of value iteration that marks useless actions to disregard them for the remainder of the computations. Our proposed approach brings an opportunity to apply some advanced techniques to reduce the running time of the computations for the interval iteration method. We consider a set of standard case studies and the experimental results show that in most cases, our proposed technique reduces the running time of computations.