Verification of the formal requirements for the system behavior based on automaton objects

The paper studies the problems of automatic verification of the behavior of a reactive system in accordance with formalized requirements, i.e., automatic verification. The reactive system is described by interconnected automaton objects. Formalized requirements are written as conditioned regular expressions. In this case mathematically reliable verification of the system is possible. The proposed solution is based on the use of the CIAO (Cooperative Interaction of Automaton Objects) language to specify the interaction of automaton objects. This paper considers the third version of the language, CIAO v.3, which defines the means of describing automaton classes, the means of instantiating automaton objects, and linking these objects to the system using a link diagram. The requirements to be verified are specified using the so-called conditioned regular expressions constructed over a set of elementary actions and conditions defined in the system. A software tool has been developed that, using a link diagram, builds a semantic graph, i.e., a directed graph, where all paths from the initial nodes represent the execution protocols of the automata-based program, thereby specifying the semantics of the reactive system. Then, it is checked whether the automata-based program complies with the requirement defined by the conditioned regular expression. If a discrepancy is detected, the tool shows the place where the semantic graph exactly does not comply with the requirement. Algorithms have been developed that allow automatic verification of reactive systems with respect to the formalized requirements of a certain class. An example of a program is given that demonstrates elevator control in the CIAO v.3 language, and the constructed reactive system is verified for compliance with formally specified requirements. The purpose of the article is to demonstrate software implementation of the tool for automatic verification of a program in the CIAO v.3 language.