ISSN 1818-1015
Министерство образования и науки Российской Федерации
Ярославский государственный университет им. П.Г. Демидова
МОДЕЛИРОВАНИЕ И АНАЛИЗ
ИНФОРМАЦИОННЫХ СИСТЕМ
Том 20 № 4 2013
Основан в 1999 г.
Выходит 6 раз в год
Свидетельство о регистрации ПИ №ФС 77-49724
выдано Федеральной службой по надзору в сфере связи,
информационных технологий и массовых коммуникаций
Главный редактор
В.А. Соколов
Редакционная коллегия
С.М. Абрамов, В.С. Афраймович (Мексика), О.Л. Бандман, В.А. Бондаренко,
С.Д. Глызин (зам. гл. ред.), А. Дехтярь (США), М.Г. Дмитриев, В.Л. Дольников,
В.Г. Дурнев, Л.С. Казарин, Ю.Г. Карпов, С.А. Кащенко, А.Ю. Колесов,
И.А. Ломазова, Г.Г. Малинецкий, В.Э. Малышкин,
А.В. Михайлов (Великобритания), В.А. Непомнящий, П.Г. Парфенов, Н.Х. Розов,
Р.Л. Смелянский, Е.А. Тимофеев (зам. гл. ред.), М.Б. Трахтенброт (Израиль),
Д.В. Тураев (Великобритания), Ф. Шнеблен (Франция)
Ответственный секретарь Е. В. Кузьмин
Адрес редакции: 150000, Ярославль, ул. Советская, 14
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
Научные статьи в журнал принимаются по электронной почте и на кафедре
теоретической информатики Ярославского государственного университета. Статьи
должны содержать УДК, аннотации на русском и английском языках и сопровождаться
набором текста в редакторе LaTEX. Плата с аспирантов за публикацию
рукописей не взимается.
○Ярославский государственный
университет им. П.Г. Демидова, 2013
c
Стр.1
СОДЕРЖАНИЕ
Моделирование и анализ информационных систем. Т. 20, №4. 2013
Построение и верификация ПЛК-программ по LTL-спецификации
Кузьмин Е.В., Соколов В.А., Рябухин Д.А.
О разрешимости бездефектности для сетей потоков работ
с неограниченным ресурсом
Башкин В.А., Ломазова И.А.
Автоматизация формирования табличных приложений
Зыкин С.В.
Алгоритм (n, t)-пороговой доверенной цифровой подписи с Арбитром
Толюпа Е.А.
К теореме Делоне о классификации схождений параллелоэдров
в гранях коразмерности 3
Магазинов А.Н.
Алгоритм замещения агентов dataflow-сети на платформе Smart-M3
Васильев А.М., Парамонов И.В., Лагутина Н.С., Мамедов Э.И.
Новый подход к множественной аутентификации пользователя
в современных разнородных информационных системах
Петров В.И., Комар М.С., Кучерявый Е.А.
Исследование ортогональности сигналов с вращением вектора поляризации
Боровков Ю.Е., Кренев А.Н., Муравьев В.Н., Омельчук А.П.
Программно-конфигурируемые сети как этап эволюции сетевых технологий
Красотин А.А., Алексеев И.В.
Тезаурус по поэтологии как инструмент для информационного поиска
и коллекции знаний
Бойков В.Н., Захаров В.Е., Каряева М.С., Соколов В.А.
Проектирование и разработка имитационной модели мультиклиентского
кластера баз данных
Бойцов Е.А.
5
23
41
55
71
81
91
104
110
125
136
Редактор, корректор А.А. Аладьева. Редактор перевода Э.И. Соколова. Подписано в печать
31.10.2013. Формат 60х841/8. Усл. печ. л. 17,2. Уч.-изд. л. 16,0. Тираж 500 экз.
Отпечатано на ризографе. Ярославский государственный университет им. П. Г. Демидова,
150 000, Ярославль, ул. Советская, 14. Телефон редакции (4852) 79-77-72.
Стр.2
ISSN 1818-1015
Ministry of Education and Science of the Russian Federation
P.G. Demidov Yaroslavl State University
MODELING AND ANALYSIS
OF INFORMATION SYSTEMS
Volume 20 No 4 2013
Founded in 1999
6 issues per year
State Registration License No ФС 77-49724
Editor-in-Chief
V. A. Sokolov
Editorial Board
S.M. Abramov, V. Afraimovich (Mexico), O.L. Bandman, V.A. Bondarenko,
S.D. Glyzin (Deputy Editor-in-Chief ), A. Dekhtyar (USA), M.G. Dmitriev, V.L. Dol’nikov,
V.G. Durnev, L.S. Kazarin, Yu.G. Karpov, S.A. Kashchenko, A.Yu. Kolesov, I.A. Lomazova,
G.G. Malinetsky, V.E. Malyshkin, A.V. Mikhailov (Great Britain), V.A. Nepomniaschy,
P.G. Parfionov, N.H. Rozov, Ph. Schnoebelen (France), R.L. Smeliansky,
E.A. Timofeev (Deputy Editor-in-Chief ), M. Trakhtenbrot (Israel), D. Turaev (Great Britain)
Responsible Secretary E. V. Kuzmin
Editorial Office Address: Sovetskaya str., 14, Yaroslavl, 150000, Russia
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
○ P.G. Demidov Yaroslavl State University, 2013
c
Стр.3
Contents
Modeling and Analysis of Information Systems. Vol. 20, No 4. 2013
Construction and Verification of PLC-programs by LTL-specification
Kuzmin E.V., Sokolov V.A., Ryabukhin D.A.
On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
Bashkin V.A., Lomazova I.A.
Automation of Tabular Applications Formation
Zykin S.V.
An Algorithm of (n, t) Threshold Proxy Signature with an Arbitrator
Tolyupa E.A.
On Delaunay’s Theorem Classifying Coincidences of Parallelohedra
at Faces of Codimension 3
Magazinov A.N.
A Substitution Algorithm for Dataflow Network Agents on Smart-M3 Platform
Vasilev A.M., Paramonov I.V., Lagutina N.S., Mamedov E.I.
A Novel Approach to Many-to-Many User Authentication
in Different Information Systems
Petrov V., Komar M., Koucheryavy Y.
Study of Orthogonal Signals to the Rotation of the Polarization Vector
Borovkov Y.E., Krenev A.N., Muravyev V.N., Omeltchuk A.P.
Software-Defined Networks as a Stage of the Network Technology Evolution
Krasotin A.A., Alexseev I.V.
Domain-Specific Thesaurus as a Tool for Information Retrieval
and Collection of Knowledge
Boikov V.N., Zakharov V.E., Karyaeva M.S., Sokolov V.A.
Designing and Development of an Imitation Model
of a Multi-Tenant Database Cluster
Boytsov E.A.
5
23
41
55
71
81
91
104
110
125
136
Стр.4
Модел. и анализ информ. систем. Т.20, №4 (2013) 5–22
c
⃝Кузьмин Е. В., Соколов В. А., Рябухин Д. А., 2013
УДК 517.9
Построение и верификация ПЛК-программ
по LTL-спецификации
Кузьмин Е. В.1, Соколов В. А.2, Рябухин Д. А.
Ярославский государственный университет им. П.Г. Демидова
150000 Россия, г. Ярославль, ул. Советская, 14
e-mail: {kuzmin,sokolov}@uniyar.ac.ru, dmitriy_ryabukhin@mail.ru
получена 20 мая 2013
Ключевые слова: программируемые логические контроллеры, технология
программирования, спецификация и верификация программ
Предлагается подход к построению и верификации программ логических
контроллеров (ПЛК) для «дискретных» задач. Спецификация программного
поведения проводится на языке темпоральной логики линейного времени LTL.
Программирование осуществляется на языке ST (Structured Text) по LTLспецификации.
Анализ корректности LTL-спецификации производится с помощью
программного средства символьной проверки модели Cadence SMV.
Предлагаемый подход к программированию и верификации программ ПЛК демонстрируется
на примере. Для дискретной задачи приводятся ST-программа,
ее LTL-спецификация и SMV-модель.
Целью статьи является описание подхода к программированию ПЛК, который
бы обеспечивал возможность анализа корректности ПЛК-программ с помощью
метода проверки модели.
Поэтому изменение значения каждой программной переменной описывается
с помощью пары LTL-формул. Первая LTL-формула описывает ситуации,
при которых происходит возрастание значения соответствующей переменной,
вторая LTL-формула задает условия, приводящие к уменьшению значения переменной.
Рассматриваемые для спецификации поведения переменных LTLформулы
являются конструктивными в том смысле, что по ним производится
построение ПЛК-программы, которая соответствует темпоральным свойствам,
выраженным этими формулами. Таким образом, программирование ПЛК сводится
к построению LTL-спецификации поведения каждой программной переменной.
Кроме этого, по LTL-спецификации строится SMV-модель, которая
затем проверяется на корректность (относительно дополнительных общепрограммных
LTL-свойств) методом проверки модели с помощью средства верификации
Cadence SMV.
1Работа проводилась при финансовой поддержке РФФИ, грант №12-01-00281-a.
2Работа проводилась при финансовой поддержке Минобрнауки РФ в рамках ФЦП «Научные
и научно-педагогические кадры инновационной России» на 2009–2013 годы, cоглашение
№14.B37.21.0392 от 06.08.2012.
5
Стр.5