Программные продукты и системы, 2014, № 2 (106)

Научно-исследовательский институт

«Центрпрограммсистем»

Программные

продукты и системы

МЕЖДУНАРОДНЫЙ НАУЧНО-ПРАКТИЧЕСКИЙ ЖУРНАЛ

№ 2 (106), 2014

Главный редактор

С.В. ЕМЕЛЬЯНОВ, академик РАН

Тверь

PROGRAMMNYE PRODUKTY 

I SISTEMY

(SOFTWARE & SYSTEMS)

International research and practice journal

no. 2 (106), 2014

Editor-in-Chief

S.V. EMELYANOV, Academician of the Russian Academy of Sciences

Tver

Russian Federation

Research Institute CENTERPROGRAMSYSTEM

 ПРОГРАММНЫЕ ПРОДУКТЫ И СИСТЕМЫ
Международное научно-практическое 
приложение к международному журналу 
«ПРОБЛЕМЫ ТЕОРИИ И ПРАКТИКИ УПРАВЛЕНИЯ»

Главный редактор 
С.В. ЕМЕЛЬЯНОВ, академик РАН (г. Москва)

Научные редакторы номера
В.П. КУПРИЯНОВ, д.э.н., профессор,
НИИ «Центрпрограммсистем» (г. Тверь)
Н.А. СЕМЕНОВ, д.т.н., профессор, ТГТУ (г. Тверь)

Рецензенты номера: 
А.Н. Сотников, д.ф.-м.н., профессор МСЦ РАН (г. Москва)
В.Н. Решетников, д.ф.-м.н., профессор МАТИ (г. Москва)
В.Б. Тарасов, к.т.н., профессор МГТУ (г. Москва)
А.Д. Цвиркун, д.т.н., профессор ИПУ РАН (г. Красноярск)
В.С. Серов, д.ф.-м.н., профессор УПН (г. Оулу, Финляндия)

Издатель НИИ «Центрпрограммсистем» (г. Тверь)

Учредители: МНИИПУ (г. Москва),

Главная редакция международного журнала 
«Проблемы теории и практики управления»

(г. Москва),

НИИ «Центрпрограммсистем» (г. Тверь)

Журнал зарегистрирован

в Комитете Российской Федерации

по печати 26 июня 1995 г.

Регистрационное

свидетельство № 013831

Подписной индекс в каталоге

Агентства «Роспечать» 70799

ISSN 0236-235X (печатн.)
ISSN 2311-2735 (онлайн)

МЕЖДУНАРОДНАЯ РЕДАКЦИОННАЯ КОЛЛЕГИЯ

Семенов Н.А. – д.т.н., профессор Тверского государственного технического университета, заместитель главного 
редактора (г. Тверь, Россия)
Решетников В.Н. – д.ф.-м.н., профессор Российского государственного технологического университета 
им. К.Э. Циолковского, заместитель главного редактора (г. Москва, Россия)
Арефьев И.Б. – д.т.н., профессор Морской академии Польши (г. Щецин, Польша)
Батыршин И.З. – д.т.н., профессор Мексиканского института нефти (г. Мехико, Мексика)
Вагин В.Н. – д.т.н., профессор Московского энергетического института (технического университета) 
(г. Москва, Россия)
Голенков В.В. – д.т.н., профессор Белорусского государственного университета информатики и радиоэлектроники 
(г. Минск, Беларусь)
Еремеев А.П. – д.т.н., профессор Московского энергетического института (технического университета)
(г. Москва, Россия)
Котов А.С. – кандидат наук, ассистент профессора университета Уэйна (штат Мичиган) (г. Детройт, США)
Кузнецов О.П. – д.т.н., профессор Института проблем управления РАН (г. Москва, Россия)
Курейчик В.М. – д.т.н., профессор Технологического института Южного федерального университета 
(г. Таганрог, Россия)
Лисецкий Ю.М. – к.т.н., генеральный директор «S&T Ukraine» (г. Киев, Украина)
Нгуен Тхань Нги – д.ф.-м.н., профессор, проректор Ханойского открытого университета (г. Ханой, Вьетнам)
Николов Р.В. – доктор наук, профессор Университета библиотековедения и информационных технологий Софии
(г. София, Болгария)
Осипов Г.С. – д.ф.-м.н., профессор, заместитель директора Института системного анализа РАН (г. Москва, Россия)
Палюх Б.В. – д.т.н., профессор Тверского государственного технического университета (г. Тверь, Россия)
Попков В.К. – д.ф.-м.н., профессор, академик МАИ (г. Новосибирск, Россия)
Рахманов A.A. – д.т.н., профессор, заместитель генерального директора Концерна «РТИ Системы» (г. Москва, Россия)
Серов В.С. – д.ф.-м.н., профессор Университета прикладных наук Оулу (г. Оулу, Финляндия)
Сотников А.Н. – д.ф.-м.н., профессор, Межведомственный суперкомпьютерный центр РАН (г. Москва, Россия)
Сулейманов Д.Ш. – академик АН Республики Татарстан, д.т.н., профессор Казанского государственного 
технического университета (г. Казань, Республика Татарстан, Россия)
Тарасов В.Б. – к.т.н., Московский государственный технический университет им. Н.Э. Баумана (г. Москва, Россия)
Хорошевский В.Ф. – д.т.н., профессор Московского физико-технического института (технического университета) 
(г. Москва, Россия)
Язенин А.В. – д.ф.-м.н., профессор Тверского государственного университета (г. Тверь, Россия)

АССОЦИИРОВАННЫЕ ЧЛЕНЫ РЕДАКЦИИ

Московский энергетический институт (технический университет), г. Москва
Технологический институт Южного федерального университета, г. Таганрог
Тверской государственный технический университет, г. Тверь
Научно-исследовательский институт «Центрпрограммсистем», г. Тверь

АДРЕС РЕДАКЦИИ

Россия, 170024, г. Тверь,
пр. 50 лет Октября, 3а
Телефон (482-2) 39-91-49

Факс (482-2) 39-91-00
E-mail: red@cps.tver.ru
www.swsys.ru

Подписано в печать 27.05.2014 г.

Отпечатано ООО ИПП «Фактор и К»

Россия, 170028, г. Тверь, ул. Лукина, д. 4, стр. 1

Заказ № 124

Выпускается один раз в квартал

Год издания двадцать седьмой

Формат 6084 1/8

Тираж 1000 экз.
Объем 200 стр.

Цена 198 руб.

Автор статьи отвечает за подбор, оригинальность и точность приводимого фактического материала.
Авторские гонорары не выплачиваются. При перепечатке материалов ссылка на журнал обязательна.

 PROGRAMMNYE PRODUKTY I SISTEMY
(SOFTWARE & SYSTEMS)

International research and practice supplement for International magazine 
THEORETICAL AND PRACTICAL ISSUES OF MANAGEMENT
Editor-in-chief
S.V. Emelyanov, Academician of the Russian Academy of Sciences (Mosсow, Russian Federation)
Science editor of the issue
V.P. Kupriyanov, Dr.Sc. (Economics), Professor, 
Research Institute CENTERPROGRAMSYSTEM (Tver, Russian Federation)
N.A. Semenov, Dr.Sc. (Engineering), Professor, TGTU (Tver, Russian Federation)
Reviewers of the issue: 
A.N. Sotnikov, Dr.Sc. (Physics and Mathematics), Professor,
JSCC of the Russian Academy of Sciences (Mosсow, Russian Federation)
V.N. Reshetnikov, Dr.Sc. (Physics and Mathematics), Professor, MATI (Mosсow, Russian Federation)
V.B. Tarasov, Ph.D. (Engineering), Professor, MSTU (Mosсow, Russian Federation)
A.D. Tsvirkun, Dr.Sc. (Engineering), Professor, IPU RAS (Mosсow, Russian Federation)
V.S. Serov, Dr.Sc. (Physics and Mathematics), Professor, 
Oulu University of Applied Sciences (Oulu, Finland)

Publisher Research Institute 

CENTERPROGRAMSYSTEM (Tver)

The Founders: International Scientific 

and Research Institute 

for Management Issues (Moscow), 

the Chief Editorial Board 

of International Magazine Theoretical 
and practical issues of management

(Moscow),

Research Institute 

CENTERPROGRAMSYSTEM (Tver)

The magazine is on record 

in Russian committee

on press 26th of June 1995

Registration certificate № 013831

ISSN 0236-235X (print)

ISSN 2311-2735 (online)

INTERNATIONAL EDITORIAL BOARD

Semenov N.A. – Dr.Sc. (Engineering), Professor of Tver State Technical University, Deputy Editor-in-Chief
(Tver, Russian Federation)
Reshetnikov V.N. – Dr.Sc. (Physics and Mathematics), Professor of Russian State Technological University (MATI), 
Deputy Editor-in-Chief (Mosсow, Russian Federation)
Arefev I.B. – Dr.Sc. (Engineering), Professor of Poland Szczecin Maritime Academy (Szczecin, Poland)
Batyrshin I.Z. – Dr.Sc. (Engineering), Professor of Mexican Institute of Petroleum (Mexico City, Mexico)
Vagin V.N. – Dr.Sc. (Engineering), Professor of Moscow Power Engineering Institute (Technical University) 
(Mosсow, Russian Federation)
Golenkov V.V. – Dr.Sc. (Engineering), Professor of Belarusian State University of Informatics and Radioelectronics (BSUIR) 
(Minsk, Republic of Belarus)
Eremeev A.P. – Dr.Sc. (Engineering), Professor of Moscow Power Engineering Institute (Technical University) 
(Moscow, Russian Federation)
Kotov A.S. – Ph.D. (Computer Science), Assistant Professor, Wayne State University (Detroit, MI, USA)
Kuznetsov O.P. – Dr.Sc. (Engineering), Professor of the Institute of Control Sciences of the Russian Academy of Sciences
(Moscow, Russian Federation)
Kureichik V.M. – Dr.Sc. (Engineering), Professor of Taganrog Technology Institute at Southern Federal University
(Taganrog, Russian Federation)
Lisetskiy Yu.M. – Ph.D.Tech.Sc., CEO of S&T Ukraine (Kiev, Ukraine)
Nguyen Thanh Nghi – Dr.Sc. (Physics and Mathematics), Professor, Vice-Principal of Hanoi Open University (Hanoi, Vietnam)
Nikolov R.V. – Full Professor of the University of Library Studies and Information Technology (Sofia, Bulgaria)
Osipov G.S. – Dr.Sc. (Physics and Mathematics), Professor, Deputy of the Principal of Institute of Systems Analysis of the 
Russian Academy of Sciences (Mosсow, Russian Federation)
Palyukh B.V. – Dr.Sc. (Engineering), Professor of Tver State Technical University (Tver, Russian Federation)
Popkov V.K. – Dr.Sc. (Physics and Mathematics), Professor, Academician of IIA (Novosibirsk, Russian Federation)
Rakhmanov A.A. – Dr.Sc. (Engineering), Professor, Deputy of the CEO of Concern RTI Systems
(Mosсow, Russian Federation)
Serov V.S. – Dr.Sc. (Physics and Mathematics), Professor of the Oulu University of Applied Sciences (Oulu, Finland)
Sotnikov A.N. – Dr.Sc. (Physics and Mathematics), Professor, Joint Supercomputer Center of the Russian Academy 
of Sciences (Moscow, Russian Federation)
Suleimanov D.Sh. – Academician of TAS, Dr.Sc. (Engineering), Professor of Kazan State Technical University
(Kazan, Republic of Tatarstan, Russian Federation)
Tarassov V.B. – Ph.D. (Engineering), Bauman Moscow State Technical University (Mosсow, Russian Federation)
Khoroshevsky V.F. – Dr.Sc. (Engineering), Professor of Moscow Institute of Physics and Technology
(Moscow, Russian Federation)
Yazenin A.V. – Dr.Sc. (Physics and Mathematics), Professor of Tver State University (Tver, Russian Federation)

ASSOCIATED EDITORIAL BOARD MEMBERS

Moscow Power Engineering Institute (Technical University), Moscow, Russian Federation
Technology Institute at Southern Federal University, Taganrog, Russian Federation
Tver State Technical University, Tver, Russian Federation
Research Institute CENTERPROGRAMSYSTEM, Tver, Russian Federation

EDITORIAL OFFICE ADDRESS
50 let Octyabrya Ave. 3а,
Tver, 170024, Russian Federation

Phone: (482-2) 39-91-49
Fax: (482-2) 39-91-00
E-mail: red@cps.tver.ru
www.swsys.ru

Passed for printing 27.05.2014

Printed in printing-office “Faktor i K”

Lukina St. 4/1, Tver, 170028, Russian Federation

Prod. order № 124
Published quarterly 

27th year of publication

Format 6084 1/8

Circulation 1000 copies

Wordage 200 pages

Price 198 rub.

Программные продукты и системы
№ 2, 2014 г.

Вниманию авторов!

Международный журнал «Программные продукты и системы» публикует материалы научного и науч
но-практического характера по новым информационным технологиям, результаты академических и отраслевых исследований в области использования средств вычислительной техники. Практикуются выпуски тематических номеров по искусственному интеллекту, системам автоматизированного проектирования, по технологии разработки программных средств и системам защиты, а также специализированные выпуски, посвященные научным исследованиям и разработкам отдельных вузов, НИИ, научных организаций. 

Решением Президиума Высшей аттестационной комиссии (ВАК) Министерства образования и науки 

РФ № 8/13 от 02.03.2012 международный журнал «Программные продукты и системы» внесен в Перечень ведущих рецензируемых научных журналов и изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней кандидата и доктора наук.

Информация об опубликованных статьях по установленной форме регулярно предоставляется в систе
му Российского индекса научного цитирования (РИНЦ) и готовится для передачи в международные базы цитирования.

Условия публикации

К рассмотрению принимаются ранее нигде не опубликованные материалы, соответствующие тематике 

журнала (специализация 05.13.ХХ – Информатика, вычислительная техника и управление) и отвечающие редакционным требованиям.

Работа представляется в электронном виде в формате Word (шрифт Times New Roman, размер 11 пунк
тов с полуторным межстрочным интервалом). При обилии сложных формул обязательно наличие статьи и в 
формате PDF. Формулы должны быть набраны в редакторе формул Word (Microsoft Equation или MathType). 
Объем статьи вместе с иллюстрациями – не менее 10 000 знаков. Просьба не присылать цветные, тонированные и не подлежащие дальнейшему редактированию средствами Word рисунки, а также отсканированные 
формулы и тексты. (Публикация материалов с использованием гипертекста, графики, аудио-, видео-, программных средств и др. возможна в нашем новом электронном издании «Программные продукты, системы и 
алгоритмы», сайт www.swsys-web.ru.) Заголовок должен быть информативным; сокращения, а также терминологию узкой тематики желательно в нем не использовать. Количество авторов на одну статью – не более 4, 
количество статей одного автора в номере, включая соавторство, – не более 2. Список литературы (оформленный в соответствии с ГОСТ Р 7.05–2008), наличие которого обязательно, должен включать не менее 5 пунктов.

Необходимы также аннотация (150–200 слов), ключевые слова (7–10) и индекс УДК. Название статьи, 

аннотация и ключевые слова должны быть переведены на английский язык (машинный перевод недопустим), 
а фамилии авторов, названия и юридические адреса организаций (если нет официального перевода), пристатейные списки литературы – транслитерированы по стандарту BGN/PCGN. 

Вместе со статьей следует прислать отзыв-рекомендацию в произвольной форме, экспертное заключе
ние, лицензионное соглашение, а также сведения об авторах: фамилия, имя, отчество, название и юридический 
адрес организации, должность, ученые степень и звание (если есть), контактный телефон, электронный адрес, 
почтовый адрес для отправки бесплатного авторского экземпляра журнала. 

Порядок рецензирования

Все статьи, поступающие в редакцию (соответствующие тематике и оформленные согласно требовани
ям к публикации), подлежат обязательному рецензированию в течение месяца с момента поступления. 

В редакции есть устоявшийся коллектив рецензентов, среди которых члены международной редколле
гии журнала, эксперты из числа крупных специалистов в области информатики и вычислительной техники ведущих вузов страны, а также ученые и специалисты НИИ «Центрпрограммсистем» (г. Тверь).

Рецензирование проводится конфиденциально. Автору статьи предоставляется возможность ознако
миться с текстом рецензии. При необходимости статья отправляется на доработку.

Рецензии обсуждаются на заседаниях рабочей группы, состоящей из членов научного совета журнала.

Заседания проводятся раз в месяц в НИИ «Центрпрограммсистем» (г. Тверь), где принимается решение о целесообразности публикации статьи.

Статьи, одобренные редакционным советом, публикуются в течение полугода с момента одобрения, 

а отправленные на доработку – с момента поступления после устранения замечаний.

Редакция международного журнала «Программные продукты и системы» в своей работе руководству
ется сводом правил Кодекса этики научных публикаций, разработанным и утвержденным Комитетом по этике научных публикаций.

Программные продукты и системы
№ 2, 2014 г.

5

УДК 519.767.2
Дата подачи статьи: 21.02.2014

АНАЛИЗ МОДЕЛЕЙ ПРОГРАММ

НА ЯЗЫКЕ АСИНХРОННЫХ ФУНКЦИОНАЛЬНЫХ СХЕМ

СРЕДСТВАМИ ТЕМПОРАЛЬНОЙ ЛОГИКИ ЛИНЕЙНОГО ВРЕМЕНИ

Ю.П. Кораблин, д.т.н., профессор; М.Л. Косакян, аспирант

(Российский государственный социальный университет, 

ул. Вильгельма Пика, 4, г. Москва, 129256, Россия, y.p.k@mail.ru, xbix@list.ru)

В статье описывается формальный метод анализа свойств параллельных и распределенных программ. Предло
жен метод верификации технических систем на выполнимость различных временных свойств, в частности, свойства
безопасности (типичный пример свойства безопасности – свобода от блокировок).

Для представления моделей технических систем в работе используется язык асинхронных функциональных схем

(АФС), в котором программе в качестве семантического значения сопоставляется множество вычислительных последовательностей (путей) выполнения распределенной АФС-программы. Далее семантическое значение представляется в виде системы рекурсивных уравнений. Полученная система является удобной формой представления семантических значений программ для анализа различных свойств программ. 

Для верификации выполнимости временных свойств семантическое значение АФС-программы, представленное 

в виде системы рекурсивных уравнений, и временное свойство, представленное как формула темпоральной логики 
линейного времени, преобразуются в автоматы Бюхи. Затем строится композиция этих автоматов, по которой проверяется выполнимость временного свойства на исходной АФС-программе. 

Предложенный в данной статье метод имеет значительное преимущество по сравнению с подобными методами, 

в которых существует промежуточный этап преобразования технической системы в систему Крипке с последующим 
представлением их в виде автомата Бюхи, тогда как в предложенном методе техническая система непосредственно 
представляется в виде автомата Бюхи.

Описанный в данной работе метод легко поддается автоматизации, что позволяет существенно упростить трудо
емкий процесс анализа семантических значений программ.

Теоретический материал статьи подкреплен рядом примеров, в частности примером применения изложенного 

метода верификации для анализа выполнимости свойства безопасности (отсутствие блокировок) распределенной 
системы 

Ключевые слова: язык асинхронных функциональных схем, система рекурсивных уравнений, верификация, вре
менная логика, автомат Бюхи, система Крипке.

ANALYSIS OF THE PROGRAMM USE THE LANGUAGE

OF ASYNCHRONOUS FUNCTIONAL SCHEMES MODELS USING LINEAR-TIME TEMPORAL LOGIC 

Korablin Yu.P., Dr.Sc. (Engineering), Professor; Kosakyan M.L., Postgraduate Student

(Russian State Social University, Vilgelma Pika St. 4, Moskow, 129256, Russian Federation, xbix@list.ru, y.p.k@mail.ru)

Received 21.02.2014

Abstract. The article describes the formal method for analyzing properties of concurrent and distributed programs. Au
thors suggest a method for verifying technical systems for various temporal properties feasibility, such as a security property 
(a typical example of security properties is lock-freedom). 

To represent models of technical systems authors use the language of asynchronous functional schemes (AFS). It in
cludes semantic values of AFS-programs represented as the sets of computing sequences (running ways of the distributed 
AFS-program). Then semantic value is represented as a system of recursive equations. This system is a convenient form for 
representing semantic values of programs to analyze various programs’ properties. 

The AFS-program semantic value, represented as a system of recursive equations, and the temporal property, represented 

as a formula linear-time temporal logic, is converted into a Büchi automata to verify the feasibility of temporal properties. 
After that the composition of these automatons is constructed. The temporary property feasibility on the original AFSprogram is verified according to this composition. 

The proposed method has a significant advantage compared to similar methods which has an intermediate stage for 

transformimg a technical system into the Kripke’s system and then converts it into a Buchi’s automaton. And in the proposed 
method the technical system directly converts into a Buchi’s automaton.

The proposed method can be easily automated. It allows to simplify essentially labor-intensive process of analyzing se
mantic values of programs.

Theoretical material of the article includes a number of examples, in particular, an example of the proposed method ap
plication for verification the feasibility of security properties (no locks) on the distributed system.

Keywords: language of asynchronous functional schemes, recursive equations system, verification, temporal logic, 

Büchi automata, Kripke system.

Как известно, любое нетривиальное ПО после 

этапа разработки содержит ошибки. Проверка современного ПО, состоящего из громадного количества строк кода, не представляется возможной. 
В связи с этим широко распространен подход, при 

котором реальные системы представляются в виде 
моделей, верифицируемых при помощи специализированного ПО. Модельный подход подразумевает частичную верификацию, которая может 
быть направлена на проверку наиболее сущест

Программные продукты и системы
№ 2, 2014 г.

6

венных свойств, абстрагировавшись от менее 
важных деталей системы. Таким образом, верификация моделей не позволяет в общем случае 
гарантировать отсутствие ошибок в реальной системе. По этой причине после этапа верификации 
модели необходим этап тестирования исходной 
системы в реальных условиях.

Для представления моделей технических сис
тем авторы статьи используют язык асинхронных функциональных схем (АФС) [1], в котором
программе в качестве семантического значения
сопоставляется множество вычислительных последовательностей (ВП) (путей) выполнения распределенной АФС-программы. Далее семантическое значение представляется в виде системы рекурсивных уравнений [1]. Полученная система 
является удобной формой представления семантических значений программ для анализа различных 
свойств программ. 

Для создания автоматизированных програм
мных средств проверки моделей необходимы 
формальные методы верификации. Одним из них 
является метод, использующий темпоральную логику линейного времени (linear-time temporal logic 
– LTL) [2]. В этом методе техническая система, 
представленная в виде структуры Крипке [2], и 
отрицание проверяемого свойства преобразуются 
в автоматы Бюхи [2]. Далее по ним строится композиция автоматов для проверки выполнимости 
проверяемого свойства на технической системе.

В данной статье предложен метод, при кото
ром системы рекурсивных уравнений, полученные 
из исходных АФС-программ, непосредственно 
представляются в виде автоматов Бюхи, что позволяет использовать описанный выше подход. 
Предложенный метод имеет преимущество над 
указанным выше методом, заключающееся в том, 
что нет необходимости в проведении дополнительного этапа преобразования системы рекурсивных уравнений в структуру Крипке. 

Язык АФС

В языке АФС программы представляются как

функции, взаимодействующие посредством интерфейса в виде каналов.

Множество АФС-программ Prog с типичным 

элементом pr определяется следующим образом:

pr ::= NET {can} BEGIN fproc END 
can ::= CHAN j::type(k):type(l) | can1 ; can2 
type ::= ALL | ANY
fproc ::= FUN i::c | fproc1 ; fproc2
c ::= a | skip | exit | break | wait(time) | read(i, l) | write(i, k)

| SEQ(c {, c}) | 

PAR(c {, c}) | ALT(gc) | LOOP(ALT(gc))
gc ::= g  c | gc {; gc}
g ::= tt | ff | b | wait(time) | read(i, l) | write(i, k)
Неформально 
семантические 
конструкции 

языка АФС можно описать так:

–
под элементарной командой a понимается 

обычное присваивание;

–
пустая команда skip не приводит к выпол
нению каких-либо действий;

–
выполнение команды exit приводит к за
вершению функционального процесса;

–
выполнение команды break приводит к за
вершению выполнения цикла;

–
команда wait(time) задерживает выполнение 

функционального процесса на время, задаваемое 
выражением time;

–
команда чтения read(i, l) осуществляет за
прос на прием данных из l-го выхода i-го канала, а 
команда write(i, k) – запрос на передачу данных на 
k-й вход i-го канала; если l-й выход (k-й вход) канала i готов к выдаче (приему) данных, то осуществляется чтение данных из канала (запись данных 
в канал), после чего функциональный процесс 
продолжается; в противном случае выполнение 
функционального процесса задерживается;

–
команда SEQ(c{, c}) означает последова
тельное 
выполнение 
команд, 
перечисленных 

внутри скобок;

–
параллельная команда PAR(c{, c}) означает 

параллельное выполнение команд, перечисленных 
внутри скобок;

–
защищенная команда gc может выпол
няться лишь в случае истинности защиты g; значение защиты g является истинным в следующих 
случаях: 1) g≡tt; 2) g≡b, причем значение b есть 
истина; 3) g≡wait(time) через интервал времени, 
задаваемый выражением time; 4) g≡read(i, l) либо 
g≡write(i, l) и соответствующий выход (вход) канала i готов к обмену; в последнем случае, если 
канал i не готов к обмену, выполнение защищенной команды приостанавливается;

–
альтернативная команда ALT(gc{; gc}) оз
начает выполнение одной из защищенных команд, 
перечисленных в скобках, для которой значения 
защит являются истинными;

–
команда цикла LOOP(ALT(gc{; gc})) озна
чает многократное выполнение альтернативной 
команды; завершение цикла осуществляется, если 
все защиты ALT-команды являются булевскими 
выражениями и ни одно из значений защит не является истинным либо при выполнении команды 
break;

–
канал типа ALL(k):ALL(l) вначале прини
мает данные по всем своим k входам, после чего 
он становится готовым для передачи данных по 
всем l выходам; канал освобождается (и становится готовым для приема новых данных) после передачи данных по всем своим выходам;

–
канал типа ALL(k):ANY(l) аналогичен по 

входу каналу типа ALL(k):ALL(l); канал освобождается после передачи данных по любому из своих 
выходов;

–
канал типа ANY(k):ALL(l) становится гото
вым для передачи данных, если он принял данные 
по одному из входов, и освобождается после передачи данных по всем своим выходам;

Программные продукты и системы
№ 2, 2014 г.

7

–
канал типа ANY(k):ANY(l) становится го
товым для передачи данных, если он принял данные по одному из входов, и освобождается после 
передачи данных по любому из своих выходов.

Формализация семантики АФС-программ.

Зададим вначале априорную семантику функциональных процессов, то есть семантику функциональных процессов без учета их взаимодействия друг с другом. Семантическая функция имеет 
вид  :FProc→SP, где FProc – множество функциональных процессов с типичным элементом 
fproc, SP – множество всех подмножеств ВП:

 ⟦fproc1;frpoc2⟧=  ⟦fproc1⟧‖  ⟦frpoc2⟧
 ⟦FUN i∷c⟧=  ⟦c⟧,

где  :Cmd→SP – функция, сопоставляющая командам языка АФС множества ВП:

 ⟦a⟧=A
 ⟦skip⟧=τ
 ⟦exit⟧=EXIT
 ⟦break⟧=BREAK 
 ⟦wait(time)⟧=TIME
 ⟦read(i, l)⟧=IN(i, l)
 ⟦write(i, k)⟧=OUT(i, k)
 ⟦SEQ(c1; c2)⟧=  ⟦c1⟧∘  ⟦c2⟧
 ⟦PAR(c1; c2)⟧=  ⟦c1⟧⫫  ⟦c2⟧
 ⟦ALT(c1; c2)⟧=  ⟦c1⟧+  ⟦c2⟧
 ⟦tt→c⟧=E⟦tt⟧^  ⟦c⟧
 ⟦tt→c⟧=E⟦ff⟧^  ⟦c⟧
 ⟦tt→c⟧=E⟦b⟧^  ⟦c⟧
 ⟦wait(time)→c⟧=  ⟦wait(time)⟧^  ⟦c⟧
 ⟦read(i, l)→c⟧=  ⟦read(i, l)⟧^  ⟦c⟧
 ⟦write(i, l)→c⟧=  ⟦write(i, l)⟧^  ⟦c⟧
 ⟦LOOP(ALT(gc))→c⟧=( ⟦ALT(gc)⟧)+

Определим семантическую функцию для вы
ражений E:Exp→SP:

E⟦tt⟧=T 
E⟦ff⟧=F 
E⟦b⟧=B

где «∘» и «^» – операции последовательной композиции ВП.

Определение 1. ВП cp называется пустой и 

обозначается через ԑ, если

1) cp≡,
2) cp≡T^ԑ.
Бесконечную последовательность вида ԑ обо
значим через ω (зацикливание).

Определение 2. ԑsp, если
1) sp≡,
2) sp=sp1+sp2 и ԑ принадлежит хотя бы одному 

из множеств – sp1 или sp2,

3) sp=sp1∘sp2 и ԑ принадлежит и sp1, и sp2 од
новременно. 

Выражение sp+ есть минимальная фиксирован
ная точка оператора F(sp), то есть sp+=μF(sp). 
Оператор F(sp) имеет вид: F(sp)=λq.  
 ∘q+ν, где

  
 
,  если 
,

\ ,  если 
,

sp
sp

sp
sp



 




,  если  
,

,  если  
.

sp
sp


 

  
 


В последнем определении символ ∆ обозначает 

выражение, значение которого зависит от среды, 
где вычисляется ∆. Выражение ∆ может прини
мать одно из двух значений:  или . Вычисление 
значения ∆ откладывается, как правило, до момента построения семантического значения всей программы целиком на основе семантических значений компонентов этой программы.

Каналам в качестве семантических значений 

сопоставляются множества ВП. Каналы можно 
рассматривать как процессы специального вида –
канальные процессы.

Канал связи интерпретируется как цикличе
ский процесс, который вначале принимает данные 
от функциональных процессов, а затем, когда все 
необходимые данные от функциональных процессов (в соответствии с логикой входов этого канала) уже приняты, передает данные функциональным процессам (в соответствии с логикой выходов 
канала).

В отличие от функциональных процессов вы
ход из канального процесса (завершение циклического процесса) невозможен. Завершение АФСпрограммы происходит при переходе всех функциональных процессов в пассивное состояние.

Семантическая функция каналов  :Can→SP

(Can – множество каналов связи с типичным элементом сan) имеет вид

 ⟦ CHAN j∷type1(k) : type2(l)⟧=((type1(IN(j, 1),

…, IN(j, k)))∘(type2 (OUT(j, 1), …, OUT(j, l) )))+.

Параметр type может принимать одно из двух 

значений: ALL или ANY.

ALL(X1, …, X2)=X1⫫X2⫫…⫫Xn, где операция ⫫

определяется следующим образом: X⫫Y=X⌊Y+Y⌊X.

Выражение X⌊Y означает то же, что и X||Y, за 

исключением того, что первым шагом будет действие из X.

Выражение p+ есть минимальная фиксирован
ная точка оператора F'(p)=λq.p∘q.

Для наглядности восприятия ВП используем 

надстрочные индексы для значений IN (OUT), характеризующих ввод (вывод) информации в канал
связи, тогда как подстрочные индексы используются для значений команд ввода (вывода) информации в функциональный процесс. Первый индекс 
в обоих случаях указывает номер канала, второй –
номер входа (выхода) канала, по которому осуществляется ввод (вывод) информации.

Для определения взаимодействия компонентов 

программы 
зададим 
частично 
определенную 

функцию

( ,
)

,
1
( ,
)

( ,
)

2
.

, если 
'
IN
(IN
) 

( 1',
2' ) 
 
и 
'
OUT
(OUT ),

в противном случае.

i k

i k
i k

i k

i k

d

C d
d
d











Семантическую функцию для АФС-программ 

обозначим как  :Prog→SP. Так, например, если 
АФС-программа имеет вид
pr=NET can1; can2; …; canm 

BEGIN fproc1;fproc2;…;fprocn END,

то
 ⟦pr⟧= ⟦can1⟧
∥ ⟦can2⟧∥⋯∥ ⟦canm⟧∥
 ⟦fproc1⟧

∥ ⟦fproc2⟧∥⋯∥ ⟦fprocn⟧.

Программные продукты и системы
№ 2, 2014 г.

8

Для построения системы рекурсивных уравне
ний, характеризующих семантическое значение 
программы, можно строить систему уравнений 
либо по выражению для  ⟦pr⟧, задающему семантическое значение всей программы целиком, либо 
на базе множества систем уравнений, характеризующих априорные семантические значения для 
составляющих компонентов АФС-программы, в 
частности для каждого функционального процесса 
и канала связи в отдельности.

Пример 1. Рассмотрим АФС-программу pr,

моделирующую задачу производитель–потребитель:
NET

CHAN1∷ALL(1):ALL(1)

BEGIN

FUN2∷LOOP(ALT(b →SEQ(write(1,1);a1))) 
FUN3 ∷LOOP(ALT(read(1,1)→a2))

END

Из данной АФС-программы получаем семан
тическое значение

 ⟦ FUN2 ∷ LOOP(ALT(b→SEQ(write(1,1);a1)))⟧=

=(B^OUT1,1∘A1)+

 ⟦ FUN3 ∷ LOOP(ALT(read(1,1)→a2)) ⟧ = (IN1,1^A2)+

F⟦ CHAN1∷ALL(1):ALL(1) ⟧ = (IN1,1 ∘ OUT1,1 )+

 ⟦pr⟧=P2‖P3‖ K1=

=(B^OUT1,1∘A1)+‖(IN1,1^A2)+‖(IN1,1∘OUT1,1 )+.

Полученное семантическое значение может 

быть представлено системой рекурсивных уравнений [1].

Обозначая элементы семантической области 

метапеременными X, Y, Z, опишем свойства семантической области с помощью следующих схем 
аксиом:
X+X=X 
X+Y=Y+X 
X+(Y+Z)=(X+Y)+Z 
(X+Y)∘Z=X∘Z+Y∘Z 
(X∘Y)∘Z=X∘(Y∘Z)
τ∘X=X 
X∘τ=X 
ω ∘X= ω
∅∘X=∅
X+∅=X 
(β^X)∘Y=β^(X∘Y) 
F^X=∅
∅^X=∅

X‖(Y||Z)=(X||Y)||Z 
X‖Y=X ⌊ Y+Y ⌊ X+ X | Y 
d1' | d2'=C(d1',d2') 
α1 | (α2∘X) = ( α1 | α2 ) ∘ X, 
если α2 ≠ τ 
(α1 ∘ X) | (α2 ∘ Y) = (α1 | α2) ∘ (X ‖ Y), 
если α1 ≠ τ, α2 ≠ τ 
α | (β^X) = (α | β)^X 
(α ∘ X) | (β ^ Y) = (α | β)^(X ‖ Y), 
если α≠τ 
(β1 ^ X) | (β2 ^ Y) = (β1 | β2 ) ^ (X ‖ Y) 
(X+Y)| Z=(X│Z)+ (Y|Z) 
τ ∘ X | Y = X | Y 
X | Y = Y |X 
α⌊X = α∘X 
α∘X⌊Y = α ∘ (X‖Y), если α≠τ 
(β^X) ⌊Y = β^(X‖Y) 
τ ∘ X ⌊Y = X ⌊Y 
(X+Y)⌊Z = X ⌊Z+Y⌊Z 
(X | Y)⌊Z = X |(Y⌊Z) 
(X ⌊ Y)⌊Z = X ⌊(Y ‖Z) 
X‖Y = X ⌊ Y+Y ⌊ X+ X | Y 

где  – останов, β – тест, ω – зацикливание.

Пример 2. Представим полученное выше се
мантическое значение АФС-программы в виде 
системы рекурсивных уравнений:

P1=B^P2+T^P3
P2=γ1,1∘P4

P3=
P4=A1∘P5+γ1,1^P6
P5=B^P7+T^P8+γ1,1^P9
P6=A1∘P9+A2∘P10
P7=γ1,1∘P11
P8=γ1,1∘P12
P9=B^P11+T^P12+A2∘P1
P10=A1∘P1
P11=γ1,1∘P13+A2∘P2
P12=A2∘P3
P13=A1∘P14+A2∘P4
P14=B^P15+T^P16+A2∘P5
P15=γ1,1∘P6+A2∘P7
P16=A2∘P8.

Автоматы Бюхи

Семантические значения, представленные в 

виде системы рекурсивных уравнений, могут быть 
заданы с помощью автомата Бюхи [2].

Автомат Бюхи – это пятерка (S, Σ, S0, δ, F), где

Σ – конечное множество символов (алфавит); S –
множество состояний; S0⊆S – множество начальных состояний (содержащее только один элемент 
для детерминированного случая); δ : S×Σ→2s – отношение переходов (для детерминированного автомата δ:S×Σ→S); F⊆S – множество финальных 
состояний.

Автомат Бюхи принимает слово, если при чте
нии этого бесконечного слова автомат проходит 
бесконечное количество раз хотя бы одно финальное состояние.

Пример 3. Представим полученную в примере 

2 систему рекурсивных уравнений (предварительно представив уравнение P3= в виде P3=∘P3) в 
виде автомата Бюхи B1 (рис. 1). Множество на
P12
P3
A2

∅

P9
P1

P16
P8

P5

P7

P10
P6
P15
P14

P13
P4
P2

P11
A2

A1
A1
B

A2
Y1,1
B

Y1,1

A1

Y1,1
A2

T

A1

B

A2

Y1,1

Y1,1

A2

A2

B
A2

Y1,1

Y1,1

T
T

T

Рис. 1. Автомат Бюхи В1, построенный по системе 

рекурсивных уравнений из примера 2

Fig. 1. Büchi automata В1 based on recursive 

equations system from example 2

Программные продукты и системы
№ 2, 2014 г.

9

чальных состояний автомата B1 включает одно состояние P1, выделенное на рисунке 1 штриховкой 
c наклоном вправо.

Описание свойств 

с помощью LTL-формул

Для проверки вычислимости тех или иных 

свойств будем описывать эти свойства в виде 
формул LTL [2].

Формулы LTL – это атомарный предикат p, 

q, …, или формулы LTL, связанные логическими
операторами ∨, ¬, или формулы LTL, связанные 
темпоральными операторами U, X.

Формально формулы LTL задаются граммати
кой φ=p|¬φ|φ∨φ|Xφ|φUφ.

Истинность формулы φ логики LTL на вычис
лении =s0, s1, … определяется индуктивно по 
формуле φ:

–
σ⊨p, если атомарный предикат p истинен в 

начальном состоянии вычисления σ;

–
σ⊨¬φ, если формула φ не истинна на σ;

–
σ⊨φ1∨φ2≡σ⊨φ1∨σ⊨φ2, если на σ выполняет
ся или φ1, или φ2;

–
σ⊨Xφ≡σ1⊨φ, если φ выполняется на вычис
лении σ1=s1, s2, …;

–
σ⊨φ1Uφ2, если когда-то в будущем состоя
нии вычисления σ выполнится формула φ2, а до ее 
выполнения во всех состояниях вычисления σ будет выполняться φ1;

–
σ⊨Fφ≡trueUφ≡(∃ k≥0) k⊨φ, если найдется 

такое k, что φ выполняется на вычислении k=sk, 
s(k+1), …;

–
σ⊨Gφ≡¬F¬φ≡(∀ k≥0) k⊨φ, если φ выпол
няется на всех состояниях вычисления σ.

Любая формула LTL φ на конкретном вычис
лении будет либо истинной, либо ложной. 

Вычисление – это бесконечная последователь
ность состояний, которые система проходит во 
времени.

Обозначим через σ(i) состояние si вычисления 

σ, а σi – вычисление, начиная с si, то есть σi=si, 
si+1, …. Тогда si⊨φ обозначает утверждение, что в
состоянии si выполняется формула φ, а σ⊨φ – что 
на вычислении σ выполняется формула φ. При 
этом полагается, что формула выполняется на вычислении σ, если она истинна в начальном состоянии последовательности σ.

Пример 4. Для проверки выполнимости свой
ства безопасности (типичный пример свойства 
безопасности – свобода от блокировок) φ=G¬ на 
системе рекурсивных уравнений из примера 2 построим (согласно алгоритму, представленному 
в [2]) автомат B¬φ (рис. 2) для формулы ¬φ=F. 
Обозначим через cl(φ) множество всех подформул 
формулы φ. Множество подформул формулы φ
называется согласованным, если существует вычисление, на котором все они могут выполняться. 
Атомы формулы φ – это максимальные множества

согласованных формул из cl(φ), которые могут 
помечать состояния вычислений [2]. Атомы можно считать состояниями искомого автомата Бюхи. 
Таким образом, в соответствии с правилами, описанными в [2], множество состояний автомата B¬φ
составляют три атома: A1={}, A2={F} и A3={, 
F}. Множество начальных состояний S0 состоит 
из двух состояний – A2 и A3, так как именно атомы 
A2 и A3 включают формулу F. Множество финальных состояний включает два состояния – A1 и 
A3. Финальные состояния автомата B¬φ (рис. 2)
заштрихованы с наклоном влево. Таким образом, 
состояние A3, которое является как начальным, так 
и финальным, выделено на рисунке 2 двойной 
штриховкой. Алфавит  автомата B¬φ состоит из 
двух символов –  и {}, где символ {} означает 
отсутствие символа , то есть если переход помечен символом {}, значит, переход выполняется по 
любому символу, отличному от . Переходы 
формируются в соответствии с правилами, описанными в [2].

Алгоритм проверки выполнимости 

LTL-формул для АФС-программ

Для проверки выполнимости LTL-формулы на 

системе рекурсивных уравнений будем использовать следующий алгоритм.

1. Представим модель технической системы 

в виде автомата Бюхи B.

2. В соответствии с алгоритмом, описанным 

в [2], построим по LTL-формуле ¬φ контрольный
автомат Бюхи B¬φ.

3. Согласно [2] построим синхронную компо
зицию автоматов B⊗ B¬φ. (Так же, как для конечных автоматов, синхронная композиция автоматов 
Бюхи – это автомат B¬φ, стоящий рядом с B и перехватывающий все входы и выходы автомата B. 
Автомат B¬φ выступает в роли контрольного автомата, работающего совместно и синхронно с B.)
Синхронная композиция автоматов B⊗B¬φ допус
A1

A3
A2

∅

∅
{}

{}
∅

{}

Рис. 2. Автомат Бюхи, построенный 

по LTL-формуле ¬φ=F

Fig. 2. Büchi automata based on LTL-formula

¬φ=F

Программные продукты и системы
№ 2, 2014 г.

10

кает пересечение языков L и L¬φ, допускаемых соответственно автоматами B и B¬φ. Следовательно,
если язык, допускаемый автоматом B⊗B¬φ, не 
пуст, значит, автомат B допускает ошибочное слово из языка L¬φ.

4. Проверим композицию автоматов B⊗B¬φ на 

наличие цикла, достижимого из начального состояния и включающего финальное состояние.
Если такой цикл имеется, значит, формула ¬φ выполняется хотя бы на одном вычислении автомата 
Бюхи B, следовательно, формула φ не выполняется на автомате Бюхи B.

Пример 5. Построим синхронную композицию 

автоматов B1⊗B¬φ (рис. 3) для пары начальных 
состояний P1 и A2 из автоматов B1 (см. пример 3)
и B¬φ (см. пример 4) соответственно. Если невыполнимость формулы φ на автомате B1⊗B¬φ показать не удастся, построим синхронную композицию автоматов B1⊗B¬φ
для пары начальных 

состояний P1 и A3. Финальными состояниями автомата B1⊗B¬φ являются такие пары состояний
PB1, AB¬φ, в которых AB¬φ – финальное состояние 
автомата B¬φ.

В композиции автоматов B1⊗B¬φ имеется цикл

(переходы, демонстрирующие наличие цикла, выделены жирной линией), достижимый из начального состояния и проходящий финальное состояние (P3, A3). Следовательно, формула ¬φ выполняется хотя бы на одном вычислении автомата B1, 
что означает невыполнимость формулы φ на исходном автомате B1. Отсюда следует, что в исходной программе существует возможность блокировки.

В заключение отметим, что в статье показан 

метод верификации выполнимости различных 
временных свойств в технических системах, представленных в виде АФС-программ. В предложенном методе осуществляется непосредственно преобразование семантического значения АФС-программы в автомат Бюхи, что, на взгляд авторов, 
является более естественным и понятным представлением технических систем по сравнению с 
их представлениями в виде структур Крипке.

Литература

1.
Кораблин Ю.П. Семантика языков распределенного 

программирования. М.: Изд-во МЭИ, 1996. 102 с.

2.
Карпов Ю.Г. Model Checking. Верификация парал
лельных и распределенных программных систем. СПб: 
БХВ-Петербург, 2010. 260 с. 

3.
Кораблин Ю.П., Кучугуров И.В., Косакян М.Л. Вопро
сы эквивалентности схем параллельных программ // Программные продукты и системы. 2011. № 4. С. 66–72.

4.
Кораблин Ю.П., Косакян М.Л., Кучугуров И.В. Вопро
сы взаимодействия и синхронизации распределенных программ на С++ с использованием Win API // Ученые записки 
РГСУ. 2013. № 1. С. 104–112. 

5.
Кларк Э.М., Грамберг О., Пелед Д. Верификация мо
делей программ: Model Checking. М.: Изд-во МЦНМО, 2002. 
416 с.

6.
Emerson E.A. Temporal and modal logic. In: J. van 

Leeuwen, ed. Handbook of Theoretical Computer Science, 1990, 
vol. B, pp. 995–1072.

7.
Giannakopoulou D., Lerda F. Efficient translation of LTL 

formulae into Buchi automata. NASA Ames Research Ceter, TR, 
2001, 17 p.

8.
Bruns G., Godefroid P. Temporal Logic Query-Checking.

Proc. 16th Ann. IEEE Symp. Logic in Computer Science, 2001,
pp. 898–914.

9.
Alur R., Dill D., Automata for modeling real-time system 

LNCS. Springer-Verlag, 1990, vol. 443, pp. 322–335.

References

1.
Korablin Yu.P. Semantika yazykov raspredelennogo pro
grammirovaniya
[Semantics of distributed programming lan
guages]. Moscow, MEI Publ., 1996, 102 p.

2.
Karpov Yu.G. Model Checking. Verifikatsiya parallelnykh 

i raspredelyonnykh programmnykh sistem [Model Checking. Verification of parallel and distributed programm systems]. St. Petersburg, BHV-Peterburg Publ., 2010, 260 p. 

3.
Korablin Yu.P., Kuchugurov I.V., Kosakyan M.L. Issues 

of parallel programs schemes equivalence. Programmnye produkty 
i sistemy [Software & Systems]. 2011, no. 4, pp. 66–72

4.
Korablin Yu.P., Kosakyan M.L., Kuchugurov I.V. Issues 

of interaction and synchronization of distributed programs on C++ 
using Win API. Uchenye zapiski RGSU [RSSU Proceedings]. 2013, 
no. 1, pp. 104–112. 

5.
Clarke E.M., Grumberg O., Peled D.A. Model Checking. 

The MIT Press, 1999, 314 p. (Russ. ed. Clarke E.M., Grumberg O., 
Peled D.A. Moscow, Moscow Center for Continuons Mathematical 
Education, 2002, 416 p.).

6.
Emerson E.A. Temporal and modal logic. Handbook of 

Theoretical Computer Science (ed. J. van Leeuwen). 1990, vol. B, 
pp. 995–1072.

7.
Giannakopoulou D., Lerda F. Efficient translation of LTL 

formulae into Buchi automata. NASA Ames Research Center, TR, 
2001, 17 p.

8.
Bruns G., Godefroid P. Temporal Logic Query-Checking. 

Proc. 16th Ann. IEEE Symp. Logic in Computer Science. 2001, 
pp. 898–914.

9.
Alur R., Dill D. Automata for modeling real-time system. 

LNCS. Springer-Verlag Publ., 1990, vol. 443, pp. 322–335.

P12, A2
P3, A3

P1, A2
P9, A2

P8, A2
P16, A2

P7, A2

P5, A2

P6, A2
P10, A2

P2, A2

P15, A2
P14, A2

P13, A2
P4, A2

P11, A2

A2

A2

A2

A2

A2

A2

A2

A1
A1
B

T
T

T

B

Y1,1

Y1,1
T

A1

B

Y1,1

Y1,1

B

A2

Ø

Y1,1

Рис. 3. Автомат Бюхи, представляющий 

синхронную композицию автоматов B1⊗B¬φ

Fig. 3. Büchi automata representing a synchronous 

composition of automata B1⊗B¬φ