ISSN 1818-1015
Министерство образования и науки Российской Федерации
Ярославский государственный университет им. П.Г. Демидова
МОДЕЛИРОВАНИЕ И АНАЛИЗ
ИНФОРМАЦИОННЫХ СИСТЕМ
Том 20 № 6 2013
Основан в 1999 году
Выходит 6 раз в год
Свидетельство о регистрации ПИ №ФС77-49724 выдано Федеральной службой
по надзору в сфере связи, информационных технологий и массовых коммуникаций
Главный редактор
В.А. Соколов,
доктор физико-математических наук, профессор, Россия
Редакционная коллегия
С.М. Абрамов, д-р физ.-мат. наук, чл.-корр. РАН, Россия; В.С. Афраймович, проф.-исследователь,
Мексика; О.Л. Бандман, д-р техн. наук, Россия; В.А. Бондаренко, д-р физ.-мат. наук,
проф., Россия; С.Д. Глызин, д-р физ.-мат. наук, проф., Россия (зам. гл. ред.); А. Дехтярь,
проф., США; М.Г. Дмитриев, д-р физ.-мат. наук, проф., Россия; В.Л. Дольников, д-р физ.мат.
наук, проф., Россия; В.Г. Дурнев, д-р физ.-мат. наук, проф., Россия; Л.С. Казарин, д-р
физ.-мат. наук, проф., Россия; Ю.Г. Карпов, д-р техн. наук, проф., Россия; С.А. Кащенко,
д-р физ.-мат. наук, проф., Россия; А.Ю. Колесов, д-р физ.-мат. наук, проф., Россия; И.А. Ломазова,
д-р физ.-мат. наук, проф., Россия; Г.Г. Малинецкий, д-р физ.-мат. наук, проф., Россия;
В.Э. Малышкин, д-р техн. наук, проф., Россия; А.В. Михайлов, д-р физ.-мат. наук,
проф., Великобритания, В.А. Непомнящий, канд. физ.-мат. наук, Россия; П.Г. Парфенов,
канд. физ.-мат. наук, доцент, Россия; Н.Х. Розов, д-р физ.-мат. наук, проф., чл.-корр. РАО,
Россия; Р.Л. Смелянский, д-р физ.-мат. наук, проф., член-корр. РАН, академик РАЕН, Россия;
Е.А. Тимофеев, д-р физ.-мат. наук, проф., Россия (зам. гл. ред.); М.Б. Трахтенброт, д-р комп.
наук, Израиль, Д.В. Тураев, проф., Великобритания, Ф. Шнеблен, проф., Франция
Ответственный секретарь Е. В. Кузьмин, д-р физ.-мат. наук, проф., Россия
Адрес редакции: 150000, Россия, Ярославль, ул. Советская, 14
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
Научные статьи в журнал принимаются по электронной почте и на кафедре теоретической
информатики Ярославского государственного университета. Статьи должны содержать УДК, аннотации
на русском и английском языках и сопровождаться набором текста в редакторе LaTEX.
Плата с аспирантов за публикацию рукописей не взимается.
○Ярославский государственный
университет им. П.Г. Демидова, 2013
c
Стр.1
СОДЕРЖАНИЕ
Моделирование и анализ информационных систем. Т. 20, №6. 2013
От редакторов специального выпуска
Глызин С.Д., Непомнящий В.А., Соколов В.А.
Общие знания в хорошо структурированных системах с абсолютной памятью
Гаранина Н.О.
Обнаружение дефектов в программном обеспечении путем объединения
ограниченной проверки моделей и аппроксимации функций
Ахин М.Х., Беляев М.А., Ицыксон В.М.
Формальная модель и задачи верификации
программно-конфигурируемых сетей
Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В.
Автоматическая верификация C-программ
на основе смешанной аксиоматической семантики
Марьясов И.В., Непомнящий В.А., Промский А.В., Кондратьев Д.А.
Автоматизация создания верифицированных тестовых сценариев
на основе гидов
Дробинцев П.Д., Котляров В.П., Летичевский А.А.
Построение и верификация LD-программ ПЛК по LTL-спецификации
Кузьмин Е.В., Соколов В.А., Рябухин Д.А.
International Conference “Geometry, Topology, and Applications”
Garber A., Edelsbrunner H., Ivanov A., Musin O., Nevskii M.
Regular Polygonal Complexes of Higher Ranks in E3
Schulte E.
On the Bootstrap for Persistence Diagrams and Landscapes
Chazal F., Fasy B.T., Lecci F., Rinaldo A., Singh A., Wasserman L.
Subword Complexes and Nil-Hecke Moves
Gorsky M. A.
A Definition of Type Domain of a Parallelotope
Grishukhin V. P.
On the Areal Random Packing
Tanemura M.
On Homology Groups of a Subspace of Triangulations of the Two-Simplex
with not More than 6 Subdivisional Boundary Vertices
Yablokova S.I.
7
10
22
36
52
64
78
95
103
111
121
129
135
142
Стр.2
Гиперболический тетраэдр: вычисление объема
с применением к доказательству формулы Шлефли
Сабитов И. Х.
Сегментация клинических эндоскопических изображений,
основанная на классификации векторных топологических признаков
Дунаева О. А., Малкова Д. Б., Мячин М.Л., Эдельсбруннер Х.
Построение оценки энтропии для специальной метрики
и произвольной функции
Tимофеева Н.Е.
Релаксационные циклы в обобщенной нейронной модели
с двумя запаздываниями
Глызин С. Д., Марушкина Е. А.
179
149
162
174
Редактор, корректор А.А. Аладьева. Редактор перевода Э.И. Соколова. Подписано в печать
30.11.2013. Формат 60х841/8. Усл. печ. л. 23,2. Уч.-изд. л. 21,5. Тираж 500 экз.
Отпечатано на ризографе. Ярославский государственный университет им. П. Г. Демидова,
150 000, Ярославль, ул. Советская, 14. Телефон редакции (4852) 79-77-72.
Стр.3
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 6 2013
Founded in 1999
6 issues per year
State Registration License No ФС 77-49724
Editor-in-Chief
V. A. Sokolov,
Doctor of Sciences in Mathematics, Professor, Russia
Editorial Board
S.M. Abramov, Prof., Dr. Sci., Corr. Member of RAS, Russia; V. Afraimovich, Prof.-researcher,
Mexico; O.L. Bandman, Prof., Dr. Sci., Russia; V.A. Bondarenko, Prof., Dr. Sci., Russia;
S.D. Glyzin, Prof., Dr. Sci., Russia (Deputy Editor-in-Chief ); A. Dekhtyar, Prof., USA;
M.G. Dmitriev, Prof., Dr. Sci., Russia; V.L. Dol’nikov, Prof., Dr. Sci., Russia; V.G. Durnev,
Prof., Dr. Sci., Russia; L.S. Kazarin, Prof., Dr. Sci., Russia; Yu.G. Karpov, Prof., Dr. Sci., Russia;
S.A. Kashchenko, Prof., Dr. Sci., Russia; A.Yu. Kolesov, Prof., Dr. Sci., Russia; I.A. Lomazova,
Prof., Dr. Sci., Russia; G.G. Malinetsky, Prof., Dr. Sci., Russia; V.E. Malyshkin, Prof.,
Dr. Sci., Russia; A.V. Mikhailov, Prof., Dr. Sci., Great Britain; V.A. Nepomniaschy, PhD, Russia;
P.G. Parfionov, PhD, Russia; N.H. Rozov, Prof., Dr. Sci., Corr. Member of RAE, Russia;
Ph. Schnoebelen, Senior Researcher, France; R.L. Smeliansky, Prof., Dr. Sci., Corr. Member of
RAS, Russia; E.A. Timofeev, Prof., Dr. Sci., Russia (Deputy Editor-in-Chief ); M. Trakhtenbrot,
Dr., Israel; D. Turaev, Prof., Great Britain
Responsible Secretary E. V. Kuzmin, Prof., Dr. Sci., Russia
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
Стр.4
Contents
Modeling and Analysis of Information Systems. Vol. 20, No 6. 2013
Common Knowledge in Well-structured Perfect Recall Systems
Garanina N.O.
Defect Detection: Combining Bounded Model Checking
and Code Contracts
Akhin M., Belyaev M., Itsykson V.
A Formal Model and Verification Problems for Software Defined Networks
Zakharov V.A., Smelyansky R.L., Chemeritsky E.V.
Automatic C Program Verification
Based on Mixed Axiomatic Semantics
Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., Kondratyev D.A.
The Guide-based Automatic Creation of Verified Test Scenarious
Drobintsev P.D., Kotlyarov V.P., Letichevsky A.A.
Construction and Verification of PLC LD-programs by LTL-specification
Kuzmin E. V., Sokolov V. A., Ryabukhin D. A.
International Conference “Geometry, Topology, and Applications”
Garber A., Edelsbrunner H., Ivanov A., Musin O., Nevskii M.
Regular Polygonal Complexes of Higher Ranks in E3
Schulte E.
On the Bootstrap for
Persistence Diagrams and Landscapes
Chazal F., Fasy B.T., Lecci F., Rinaldo A., Singh A., Wasserman L.
Subword Complexes and Nil-Hecke Moves
Gorsky M. A.
A Definition of Type Domain of a Parallelotope
Grishukhin V. P.
On the Areal Random Packing
Tanemura M.
On Homology Groups of a Subspace of Triangulations of the Two-Simplex
with not More than 6 Subdivisional Boundary Vertices
Yablokova S.I.
Hyperbolic Tetrahedron: Volume Calculation with Application
to the Proof of the Schl¨
Sabitov I.Kh.
afli Formula
149
10
22
36
52
64
78
95
103
111
121
129
135
142
Стр.5