title: ÐÑÐ¿Ð¾Ð»ÑÐ·Ð¾Ð²Ð°Ð½Ð¸Ðµ Ð¾Ð±ÑÑÐ»Ð¾Ð²Ð»ÐµÐ½Ð½ÑÑ ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÑ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸Ð¹ Ð´Ð»Ñ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ½ÑÑ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼
title: Ð²ÑÐ¿ÑÑÐºÐ½Ð°Ñ ÐºÐ²Ð°Ð»Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¾Ð½Ð½Ð°Ñ ÑÐ°Ð±Ð¾ÑÐ° Ð¼Ð°Ð³Ð¸ÑÑÑÐ°
titleType: Subtitle
title: The use of conditional regular expressions for verification automata-based programs
Creators: name: Ð¥Ð°ÑÐ¸ÑÐ¾Ð²Ð°, Ð¢Ð°Ð¸ÑÐ¸Ñ
Publisher: name: Ð¡Ð°Ð½ÐºÑ-ÐÐµÑÐµÑÐ±ÑÑÐ³ÑÐºÐ¸Ð¹ Ð¿Ð¾Ð»Ð¸ÑÐµÑÐ½Ð¸ÑÐµÑÐºÐ¸Ð¹ ÑÐ½Ð¸Ð²ÐµÑÑÐ¸ÑÐµÑ ÐÐµÑÑÐ° ÐÐµÐ»Ð¸ÐºÐ¾Ð³Ð¾
Year: 2024
Subjects: ÐÑÑÐ¸ÑÐ»Ð¸ÑÐµÐ»ÑÐ½ÑÐµ Ð¼Ð°ÑÐ¸Ð½Ñ ÑÐ»ÐµÐºÑÑÐ¾Ð½Ð½ÑÐµ
Ð¼ÐµÑÐ¾Ð´Ñ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸
ÑÐµÐ°Ð³Ð¸ÑÑÑÑÐ¸Ðµ ÑÐ¸ÑÑÐµÐ¼Ñ
Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ½Ð¾Ðµ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð¸ÑÐ¾Ð²Ð°Ð½Ð¸Ðµ
Ð¾Ð±ÑÑÐ»Ð¾Ð²Ð»ÐµÐ½Ð½ÑÐµ ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÐµ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸Ñ
Ð³ÑÐ°Ñ Ð¿ÐµÑÐµÑ Ð¾Ð´Ð¾Ð² ÑÐ¾ÑÑÐ¾ÑÐ½Ð¸Ð¹
verification methods
reactive systems
automata-based programming
conditional regular expressions
state transition graph

description: ÐÐ°Ð½Ð½Ð°Ñ ÑÐ°Ð±Ð¾ÑÐ° Ð¿Ð¾ÑÐ²ÑÑÐµÐ½Ð° Ð¸Ð·ÑÑÐµÐ½Ð¸Ñ Ð¼ÐµÑÐ¾Ð´Ð° Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ ÑÐ°ÑÐ¿ÑÐµÐ´ÐµÐ»ÐµÐ½Ð½ÑÑ Ð¸ Ð¿Ð°ÑÐ°Ð»Ð»ÐµÐ»ÑÐ½ÑÑ ÑÐµÐ°Ð³Ð¸ÑÑÑÑÐ¸Ñ ÑÐ¸ÑÑÐµÐ¼, Ð¾Ð¿Ð¸ÑÐ°Ð½Ð½ÑÑ Ð½Ð° ÑÐ·ÑÐºÐµ CIAO v.3, Ð° ÑÐ°ÐºÐ¶Ðµ Ð¸ÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ñ ÑÐ¿Ð¾ÑÐ¾Ð±Ð¾Ð² Ð·Ð°Ð´Ð°Ð½Ð¸Ñ ÑÑÐµÐ±Ð¾Ð²Ð°Ð½Ð¸Ð¹ Ðº ÑÐ°ÐºÐ¸Ð¼ ÑÐ¸ÑÑÐµÐ¼Ð°Ð¼ Ð² ÑÐ¾ÑÐ¼Ðµ Ð¾Ð±ÑÑÐ»Ð¾Ð²Ð»ÐµÐ½Ð½ÑÑ ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÑ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸Ð¹. ÐÐ°Ð´Ð°ÑÐ¸, ÐºÐ¾ÑÐ¾ÑÑÐµ ÑÐµÑÐ°Ð»Ð¸ÑÑ Ð² ÑÐ¾Ð´Ðµ ÑÐ°Ð±Ð¾ÑÑ: 1. ÐÑÑÐ»ÐµÐ´Ð¾Ð²Ð°Ð½Ð¸Ðµ Ð¼ÐµÑÐ¾Ð´Ð° Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼, Ð¾Ð¿Ð¸ÑÐ°Ð½Ð½ÑÑ Ð½Ð° ÑÐ·ÑÐºÐµ CIAO, Ð¸ ÑÑÐ°Ð²Ð½ÐµÐ½Ð¸Ðµ Ñ Ð´ÑÑÐ³Ð¸Ð¼Ð¸ Ð¼ÐµÑÐ¾Ð´Ð°Ð¼Ð¸ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸. 2. Ð Ð°ÑÑÐ¼Ð¾ÑÑÐµÐ½Ð¸Ðµ Ð¿Ð¾Ð´ÑÐ¾Ð´Ð¾Ð² Ðº Ð´Ð¾Ð±Ð°Ð²Ð»ÐµÐ½Ð¸Ñ ÑÑÐ¾ÑÐ¾Ð¶ÐµÐ²ÑÑ ÑÑÐ»Ð¾Ð²Ð¸Ð¹ Ð² ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÐµ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸Ñ Ð¸ ÑÐ°Ð·ÑÐ°Ð±Ð¾ÑÐºÐ° Ð¼ÐµÑÐ¾Ð´Ð¾Ð² ÑÐ°Ð±Ð¾ÑÑ Ñ Ð½Ð¸Ð¼Ð¸. 3. Ð Ð°Ð·ÑÐ°Ð±Ð¾ÑÐºÐ°, ÑÐµÐ°Ð»Ð¸Ð·Ð°ÑÐ¸Ñ Ð¸ Ð°Ð¿ÑÐ¾Ð±Ð°ÑÐ¸Ñ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð° Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸. Ð ÑÐµÐ·ÑÐ»ÑÑÐ°ÑÐµ Ð¿ÑÐµÐ´Ð»Ð¾Ð¶ÐµÐ½Ñ Ð´Ð²Ð° Ð¿Ð¾Ð´ÑÐ¾Ð´Ð° Ðº Ð´Ð¾Ð±Ð°Ð²Ð»ÐµÐ½Ð¸Ñ ÑÑÐ¾ÑÐ¾Ð¶ÐµÐ²ÑÑ ÑÑÐ»Ð¾Ð²Ð¸Ð¹ Ð² ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÐµ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸Ñ: Ð¿ÑÐ¸ Ð¿ÐµÑÐ²Ð¾Ð¼ Ð¿Ð¾Ð´ÑÐ¾Ð´Ðµ ÑÑÐ¾ÑÐ¾Ð¶ÐµÐ²Ð¾Ðµ ÑÑÐ»Ð¾Ð²Ð¸Ðµ ÑÐ°ÑÑÐ¼Ð°ÑÑÐ¸Ð²Ð°ÐµÑÑÑ ÐºÐ°Ðº ÑÐ¸Ð¼Ð²Ð¾Ð» Ð°Ð»ÑÐ°Ð²Ð¸ÑÐ°, Ð¿ÑÐ¸ Ð²ÑÐ¾ÑÐ¾Ð¼ Ð¿Ð¾Ð´ÑÐ¾Ð´Ðµ ÑÑÐ¾ÑÐ¾Ð¶ÐµÐ²Ð¾Ðµ ÑÑÐ»Ð¾Ð²Ð¸Ðµ Ð½Ðµ ÑÐ²Ð»ÑÐµÑÑÑ ÑÐ¸Ð¼Ð²Ð¾Ð»Ð¾Ð¼ Ð°Ð»ÑÐ°Ð²Ð¸ÑÐ°. ÐÐ±Ð° Ð¿Ð¾Ð´ÑÐ¾Ð´Ð° Ð¼Ð¾Ð³ÑÑ Ð±ÑÑÑ Ð¸ÑÐ¿Ð¾Ð»ÑÐ·Ð¾Ð²Ð°Ð½Ñ Ð² Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ðµ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸. ÐÑÐµÐ´Ð»Ð¾Ð¶ÐµÐ½Ñ Ð¼ÐµÑÐ¾Ð´Ñ ÑÐ°Ð±Ð¾ÑÑ Ñ Ð¾Ð±ÑÑÐ»Ð¾Ð²Ð»ÐµÐ½Ð½ÑÐ¼Ð¸ ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÐ¼Ð¸ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸ÑÐ¼Ð¸ Ð´Ð»Ñ Ð¾Ð±Ð¾Ð¸Ñ Ð¿Ð¾Ð´ÑÐ¾Ð´Ð¾Ð². ÐÐ¾Ð´ÑÐ¾Ð±Ð½Ð¾ ÑÐ°ÑÑÐ¼Ð¾ÑÑÐµÐ½ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð¸ Ð¿ÑÐ¸Ð²ÐµÐ´ÐµÐ½Ð° ÐµÐ³Ð¾ ÑÐµÐ°Ð»Ð¸Ð·Ð°ÑÐ¸Ñ Ñ Ð¸ÑÐ¿Ð¾Ð»ÑÐ·Ð¾Ð²Ð°Ð½Ð¸ÐµÐ¼ Ð¾Ð´Ð½Ð¾Ð³Ð¾ Ð¸Ð· Ð¿Ð¾Ð´ÑÐ¾Ð´Ð¾Ð² Ðº ÑÐ°Ð±Ð¾ÑÐµ Ñ Ð¾Ð±ÑÑÐ»Ð¾Ð²Ð»ÐµÐ½Ð½ÑÐ¼Ð¸ ÑÐµÐ³ÑÐ»ÑÑÐ½ÑÐ¼Ð¸ Ð²ÑÑÐ°Ð¶ÐµÐ½Ð¸ÑÐ¼Ð¸. ÐÑÐ¸Ð²ÐµÐ´ÐµÐ½Ñ Ð¿ÑÐ¸Ð¼ÐµÑÑ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼, Ð¾Ð¿Ð¸ÑÐ°Ð½Ð½ÑÑ Ð½Ð° ÑÐ·ÑÐºÐµ CIAO, Ð±Ð»Ð°Ð³Ð¾Ð´Ð°ÑÑ ÑÐµÐ¼Ñ Ð¿ÑÐ¾Ð´ÐµÐ¼Ð¾Ð½ÑÑÑÐ¸ÑÐ¾Ð²Ð°Ð½Ð° Ð²Ð¾Ð·Ð¼Ð¾Ð¶Ð½Ð¾ÑÑÑ Ð¿ÑÐ¾Ð²ÐµÐ´ÐµÐ½Ð¸Ñ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¸ Ð°Ð²ÑÐ¾Ð¼Ð°ÑÐ¸ÑÐµÑÐºÐ¸ Ñ Ð¸ÑÐ¿Ð¾Ð»ÑÐ·Ð¾Ð²Ð°Ð½Ð¸ÐµÐ¼ ÑÐµÐ°Ð»Ð¸Ð·Ð¾Ð²Ð°Ð½Ð½Ð¾Ð³Ð¾ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð°.
description: 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.