ISSN 1818-1015
Министерство образования и науки Российской Федерации
Ярославский государственный университет им. П.Г. Демидова
МОДЕЛИРОВАНИЕ И АНАЛИЗ
ИНФОРМАЦИОННЫХ СИСТЕМ
Том 18 № 4 2011
Основан в 1999 г.
Выходит 4 раза в год
Свидетельство о регистрации №019209 от 16.08.99
Государственного Комитета Российской Федерации по печати
Главный редактор
В.А. Соколов
Редакционная коллегия
С.М. Абрамов, О.Л. Бандман, В.А. Бондаренко, И.Б. Вирбицкайте,
С.Д. Глызин (зам. гл. ред.), М.Г. Дмитриев, В.Л. Дольников, В.Г. Дурнев,
А.В. Зафиевский, Л.С. Казарин, Ю.Г. Карпов, С.А. Кащенко, А.Ю. Колесов,
И.А. Ломазова, В.Э. Малышкин, В.А. Непомнящий,
П.Г. Парфенов, Р.Л. Смелянский
Ответственный секретарь Е.А. Тимофеев
Адрес редакции: 150000, Ярославль, ул. Советская, 14
E-mail: mais@uniyar.ac.ru
Website: mais.uniyar.ac.ru
Научные статьи в журнал принимаются по электронной почте и на кафедре
теоретической информатики Ярославского государственного университета. Статьи
должны содержать УДК, аннотации на русском и английском языках и сопровождаться
набором текста в редакторе LaTEX. Плата с аспирантов за публикацию
рукописей не взимается.
Ярославский государственный
университет им. П.Г. Демидова, 2011
c
Стр.1
СОДЕРЖАНИЕ
Моделирование и анализ информационных систем. Т. 18, №4. 2011
От редакторов специального выпуска
Непомнящий В.А., Соколов В.А.
Типовые примеры использования языка Atoment
Ануреев И.С.
Атрибутные аннотации и их применение в дедуктивной верификации C-программ
Атучин М.М., Ануреев И.С.
Построение приближений бисимуляции в односчетчиковых сетях
Башкин В.А.
Статический анализ с использованием систем типов и эффектов на основе LLVM
Беляев М.А., Цесько В. А.
Оптимизационные процедуры в аффинной проверке моделей
Гаранина Н.О.
Использование зависимостей для повышения точности статического анализа программ
Глухих М.И., Ицыксон В. М., Цесько В. А.
Ингибиторная сеть Петри, выполняющая произвольный заданный нормальный
алгорифм Маркова
Зайцев Д.А.
Автоматическое обнаружение ошибок конкурентной модификации данных
в моделях на языке SystemC
Захаров А.В., Моисеев М.Ю.
Простой алгоритм решения задачи покрытия для монотонных счетчиковых систем
Климов Анд.В.
Формальная модель требований, используемая в процессе генерации кода приложения
и кода тестов
Баранов С.Н., Котляров В.П.
Тестирование безопасности программного обеспечения на языке С с использованием
верификатора SPIN
Кушик Н.Г., Маммар А., Кавалли А., Евтушенко Н.В., Джиминез В.,
Монте де Ока Е.
Верификация телекоммуникационных систем, специфицированных взаимодействующими
конечными автоматами, с помощью раскрашенных сетей Петри
Белоглазов Д.М., Машуков М.Ю., Непомнящий В.А.
Верификация шаблонов алгоритмов для метода отката и метода ветвей и границ
Шилов Н.В.
Редактор, корректор А.А. Аладьева. Редактор перевода Э.И. Соколова. Подписано в печать
25.01.2012. Формат 60х841/8. Усл. печ. л. 20,2. Уч.-изд. л. 18,5. Тираж 500 экз. Заказ 022/012
Отпечатано на ризографе. Ярославский государственный университет им. П. Г. Демидова,
150 000, Ярославль, ул. Советская, 14. Телефон редакции (4852) 79-77-72.
5
7
21
34
45
56
68
80
94
106
118
131
144
Верификация Си-программ: объяснение условий корректности и стандартная библиотека
Промский А.В.
157
168
Стр.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 18 No 4 2011
Founded in 1999
4 issues per year
State Registration License No 019209 of 16.08.1999
Editor-in-Chief
V. A. Sokolov
Editorial Board
S.M. Abramov, O.L. Bandman, V.A. Bondarenko, I.B. Virbitskayte,
S.D. Glyzin (Deputy Editor-in-Chief ), M.G. Dmitriev, V.L. Dol’nikov,
V.G. Durnev, A.V. Zafievsky, L.S. Kazarin, Yu.G. Karpov,
S.A. Kashchenko, A.Yu. Kolesov, I.A. Lomazova,
V.E. Malyshkin, V.A. Nepomniaschy, P.G. Parfionov, R.L. Smeliansky
Responsible Secretary E. A. Timofeev
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, 2011
c
Стр.3
Contents
Modeling and Analysis of Information Systems. Vol. 18, No 4. 2011
Typical Examples of Atoment Language Using
Anureev I.S.
Attribute Annotations and Their Use in C Program Deductive Verification
Atuchin M.M., Anureev I.S.
Approximating Bisimulation in One-counter Nets
Bashkin V.A.
LLVM-based Static Analysis Tool Using Type and Effect Systems
Belyaev M.A., Tsesko V. A.
Optimization Procedures in Affine Model Checking
Garanina N.O.
The Use of Dependencies for Improving the Precision of Program Static Analysis
Glukhikh M.I., Itsykson V. M., Tsesko V. A.
Inhibitor Petri Net that Executes an Arbitrary Given Markov Normal Algorithm
Zaitsev D.A.
Automatic Data Race Error Detection in SystemC Models
Zakharov A.V., Moiseev M.J.
A Simple Algorithm for Solving the Coverability Problem for Monotonic Counter Systems
Klimov And.V.
A Formal Requirements Model, Used in the Process of Application Code
and Test Code Generation
Baranov S.N., Kotlyarov V.P.
A SPIN-based Approach for Detecting Vulnerabilities in C Programs
Kushik N.G., Mammar A., Cavalli A., Yevtushenko N.V., Jimenez W.,
Montes de Oca E.
Verification of Telecommunication Systems Specified by Communicating Finite Automata
with the Help of Coloured Petri Nets
Beloglazov D.M., Mashukov M.Yu., Nepomniaschy V.A.
C Program Verification: VC Explanation and the Standard Library
Promsky A. V.
Verification of Backtracking and Branch and Bound Design Templates
Shilov N.V.
7
21
34
45
56
68
80
94
106
118
131
144
157
168
Стр.4
От редакторов специального выпуска
В.А. Непомнящий, В.А. Соколов
Данный выпуск представляет статьи, подготовленные на основе избранных докладов
Второго международного семинара "Семантика, спецификация и верификация программ:
теория и приложения" (Second Workshop on Program Semantics, Specification and
Verification: Theory and Applications, PSSV 2011). Этот семинар был проведен 12 – 13 июня
2011 года в городе Санкт-Петербурге в рамках 6-го Международного симпозиума по компьютерным
наукам в России (6th International Computer Science Symposium in Russia, CSR
2011). Его труды, содержащие краткое изложение 17 докладов, опубликованы в сборнике,
изданном в Ярославском государственном университете. Тематика семинара включала направления
исследований, относящиеся к изучению моделей, применяемых для анализа и
верификации программных систем, таких как автоматные модели и сети Петри, методам
дедуктивной верификации программ, методу проверки моделей (model checking method),
формальным подходам к тестированию и валидации программ, а также к разработке и
применению систем тестирования и верификации.
Настоящий выпуск включает 14 статей. Теоретическим проблемам посвящены 5 статей.
В статье В.А. Башкина "Построение приближений бисимуляции в односчетчиковых
сетях" рассматриваются конечные автоматы с дополнительным целочисленным неотрицательным
счетчиком, названные односчетчиковыми сетями. Представлен метод приближения
наибольшей бисимуляции в односчетчиковых сетях.
В статье Н.О. Гараниной "Оптимизационные процедуры в аффинной проверке моделей"
предложены алгоритмы оптимизации аффинных представлений данных, которые
могут использоваться в методе символьной проверки моделей.
В статье Д.А. Зайцева "Ингибиторная сеть Петри, выполняющая произвольный заданный
нормальный алгорифм Маркова" описана процедура, которая по заданному нормальному
алгорифму Маркова строит ингибиторную сеть Петри, выполняющую данный
алгорифм.
В статье А. В. Климова "Простой алгоритм решения задачи покрытия для монотонных
счетчиковых систем" предложен и обоснован новый алгоритм решения задачи покрытия
для монотонных счетчиковых систем.
В статье Н.В. Шилова "Верификация шаблонов алгоритмов для метода отката и метода
ветвей и границ" описаны шаблоны алгоритмов для метода отката и метода ветвей и
границ и доказана методом Флойда корректность этих шаблонов при определенных ограничениях.
6
статей посвящено разработке теоретических методов и экспериментальных подходов,
ориентированных на практические применения.
В статье И.С. Ануреева "Типовые примеры использования языка Atoment" описан новый
предметно-ориентированный язык выполнимых спецификаций Atoment, предназначенный
для описания метода и техник верификаций программ, и представлена коллекция
типовых примеров использования языка Atoment.
В статье М.М. Атучина и И.С. Ануреева "Атрибутные аннотации и их применение
в дедуктивной верификации C-программ" предложен новый вид аннотаций, называемых
атрибутными аннотациями, и описана методология их применения в дедуктивной верификации
С-программ.
В статье С.Н. Баранова и В.П.Котлярова "Формальная модель требований, используемая
в процессе генерации кода приложения и кода тестов" предложена формальная
5
Стр.5