Вельдер С.Э. и др. Верификация автоматных программ
Подождите немного. Документ загружается.
240
Алфавитный указатель
—C—
CTL-модель, 76, 83
—L—
LTL-модель, 37, 124
LTL-таблица, 50, 99
—А—
автомат
Бюхи, 62, 99, 100
временной, 110
незенонов, 118, 142
расходящийся, 118, 142
регионный, 128, 135, 137
автоматное программирование, 170,
229
аксиоматизация, 44
активный оператор, 151
арность, 27
атомарное предложение, 30
—Б—
безопасность, 34
бинарная разрешающая диаграмма,
91, 92
блокированный оператор, 152
—В—
валидация систем, 5, 9
варианта, 19
верификация
глобальная задача, 91
локальная задача, 91
формальная, 15, 228
ветвящаяся темпоральная логика, 35,
72
реального времени, 108
временная сеть Петри, 147
временной автомат, 110
—Г—
глобальная задача верификации, 91
глубина формулы, 138
темпоральная, 86
граф достижимости сети Петри, 146
—Д—
двоичная разрешающая диаграмма,
91, 92
достижимое состояние
временного автомата, 117
сети Петри, 148
дуга сети Петри, 145
—Ж—
живучесть, 34
—З—
задача
выполнимости, 42
тавтологичности, 42
зенонов путь, 118
—И—
инвариант
позиции, 111
цикла, 18
интервал запуска, 147
—К—
комбинаторный взрыв, 26, 228
константа, 27
корректность, 44
кратность дуги, 145
—Л—
линейная темпоральная логика, 35,
72
локальная задача верификации, 91
241
—М—
маркированная сеть, 146
метод
полного графа переходов, 206
редуцированного графа переходов,
210
модель Крипке, 31, 83, 99
мок-объект, 14
—Н—
начальное состояние
автомата Бюхи, 62
временного автомата, 116, 127
временной сети Петри, 148
модели Крипке, 31, 50, 54
незенонов автомат, 118, 142
немаркированная сеть, 146
неограниченный регион, 137
нестрогая интерпретация, 45
—О—
оператор
активный, 151
блокированный, 152
будущего, 46
предшествования, 46, 124
темпоральный, 36
отношение
выполняемости, 38, 77, 90, 115
тотальное, 31, 76, 99
отсутствие голодания, 166, 169
оценка, 31
часовая, 114
—П—
переход
автомата Бюхи, 62
модели Крипке, 31
сети Петри, 145
позиция
временного автомата, 110, 111
пути, 117
сети Петри, 145
полнота, 45
последовательность запусков, 146
постусловие, 16
потомок, 38
задержки, 136
прямой, 38
правило вывода, 16
предикат, 27
предложение, 27
атомарное, 30
предусловие, 16
проверка моделей, 6, 21, 148, 228
ограниченной глубины, 228
символьная, 228
прогресс, 48, 169
произведение автоматов, 174
прямой потомок, 38
путь
в модели Крипке, 31, 76
во временном автомате, 117
зенонов, 118
расходящийся, 117
сходящийся, 117
—Р—
разметка сети, 145
разработка через тестирование, 14
расходящийся
автомат, 118, 142
путь, 117
реактивная система, 11, 34
242
регион, 128, 134
неограниченный, 137
регионный автомат, 128, 135, 137
—С—
сеть, 145
маркированная, 146
немаркированная, 146
Петри, 146
Петри, временная, 147
символьная проверка моделей, 228
симуляция, 12
система
критичная ко времени, 107
реактивная, 11, 34
трансформирующая, 34
система переходов
временного автомата, 116
временной сети Петри, 148
состояние
LTL-модели, 37
автомата Бюхи, 62
временного автомата, 114, 122
временной сети Петри, 147
достижимое, 117, 148
модели Крипке, 31
начальное, 31, 50, 54, 62, 116, 127,
148
справедливость, 53, 70, 89, 93, 168
строгая интерпретация, 45
структура Крипке, 31
суффикс пути, 76, 84
сходящийся путь, 117
—Т—
темпоральная логика, 21
ветвящаяся, 35, 72
линейная, 35, 72
реального времени, 108
темпоральный оператор, 36
терм, 27
тест, 12
тестирование, 12
типизированная логика, 28
тотально корректная формула, 16
тотальное отношение, 31, 76, 99
трансформирующая система, 34
тройка Хоара, 16
—У—
утверждения (assertions), 160, 175
—Ф—
фиксирующий идентификатор, 120
формальная верификация, 15, 228
формальная система, 16
формула
пути, 82
состояния, 82
формульные часы, 120
—Ч—
часовая оценка, 114
часовое ограничение, 110
частично корректная формула, 16
часы, 110
формульные, 120
—Э—
эквивалентность
выразительная, 84
формул, 84
—Я—
язык модели, 60
В 2009 году Университет стал победителем многоэтапного конкурса, в
результате которого определены 12 ведущих университетов России,
которым присвоена категория «Национальный исследовательский
университет». Министерством образования и науки Российской
Федерации была утверждена Программа развития государственного
образовательного учреждения высшего профессионального
образования «Санкт-Петербургский государственный университет
информационных технологий, механики и оптики» на 2009–2018 годы.
КАФЕДРА КОМПЬЮТЕРНЫХ ТЕХНОЛОГИЙ
Кафедра компьютерных технологий была основана в 1991 году по
инициативе профессоров В. Н. Васильева и В. Г. Парфенова для
проведения специального образовательного проекта, имеющего целью
создание сквозной школьно-вузовской системы отбора, подготовки и
трудоустройства одаренных в области точных наук школьников и
студентов. За прошедшие два десятилетия проект получил широкую
известность и многочисленные положительные отзывы российских и
зарубежных специалистов. В настоящее время на кафедре
компьютерных технологий обучается порядка 200 студентов, более
половины из которых являются победителями региональных олимпиад
по точным наукам, а около семидесяти – победителями
Международных и Всероссийских олимпиад по математике, физике и
информатике.
По качеству студенческого и преподавательского состава и
техническому оснащению компьютерной техникой кафедра
компьютерных технологий относится к числу лучших российских
специализированных компьютерных кафедр.
Сергей Эдуардович Вельдер,
Михаил Андреевич Лукин,
Анатолий Абрамович Шалыто,
Булат Равилевич Яминов
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ
Учебное пособие
В авторской редакции
Дизайн и верстка С. Э. Вельдер
Редакционно-издательский отдел
Санкт-Петербургского государственного университета
информационных технологий, механики и оптики
Зав. РИО Н. Ф. Гусарова
Лицензия ИД № 00408 от 05.11.99
Подписано к печати 27.01.2011 г.
Заказ № 1527
Тираж 150 экз.
Учреждение «Университетские Телекоммуникации»
«Типография на Биржевой»
199034, СПб, В.О., Биржевая линия, д. 14–16
тел.: +7 (812) 915-14-54, e-mail: zakaz@TiBir.ru
www.TiBir.ru
Редакционно-издательский отдел
Санкт-Петербургского государственного
университета информационных технологий,
механики и оптики
197101, Санкт-Петербург, Кронверкский пр., 49