Details

Данная работа посвящена изучению метода верификации распределенных и параллельных реагирующих систем, описанных на языке CIAO v.3, а также исследованию способов задания требований к таким системам в форме обусловленных регулярных выражений. Задачи, которые решались в ходе работы: 1. Исследование метода верификации программ, описанных на языке CIAO, и сравнение с другими методами верификации. 2. Рассмотрение подходов к добавлению сторожевых условий в регулярные выражения и разработка методов работы с ними. 3. Разработка, реализация и апробация алгоритма верификации. В результате предложены два подхода к добавлению сторожевых условий в регулярные выражения: при первом подходе сторожевое условие рассматривается как символ алфавита, при втором подходе сторожевое условие не является символом алфавита. Оба подхода могут быть использованы в алгоритме верификации. Предложены методы работы с обусловленными регулярными выражениями для обоих подходов. Подробно рассмотрен алгоритм верификации и приведена его реализация с использованием одного из подходов к работе с обусловленными регулярными выражениями. Приведены примеры верификации программ, описанных на языке CIAO, благодаря чему продемонстрирована возможность проведения верификации автоматически с использованием реализованного алгоритма.

The given work is devoted to the study of the verification method for distributed and parallel reactive systems described in the CIAO v.3 language and the research of techniques to set requirements for such systems in the form of conditional regular expressions. The research set the following goals: 1. Investigation the verification method for the program described in the CIAO language and comparing it with other verification methods. 2. Consideration of approaches to adding guard conditions to regular expressions and the development of methods for working with them. 3. Development, implementation and approbation of the verification method. As a result, two approaches to adding guard conditions to regular expressions are proposed: in the first approach, the guard condition is considered a symbol of the alphabet; in the second approach, the guard condition is not a symbol of the alphabet. Both approaches can be used in the verification algorithm. Methods of working with conditional regular expressions for both approaches were proposed. The verification algorithm was considered in detail, and its implementation using one of the approaches to working with conditional regular expressions was presented. Examples of verification of programs described in the CIAO language were provided, demonstrating the possibility of performing verification automatically using the implemented algorithm.