Кларк Э.М., Грамберг О., Пелед Д. — Верификация моделей программ: Model Checking :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Кларк Э.М., Грамберг О., Пелед Д. — Верификация моделей программ: Model Checking

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Верификация моделей программ: Model Checking

Авторы: Кларк Э.М., Грамберг О., Пелед Д.

Аннотация:

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

Язык:

Рубрика: Математика/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 2002

Количество страниц: 416

Добавлена в каталог: 08.11.2009

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

Отношение дизъюнктивно расщеплённое (disjunctive partitioned)      119
Отношение зависимости (dependency)      197
Отношение конъюнктивно расщеплённое (conjunctive partitioned)      119
Отношение независимости (independence relation)      201
Отношение орбит (orbit relation)      294
Отношение переходов (transition)      40 158 172 197
Отношение расщеплённое (partitioned)      119
Отношение симуляции (simulation)      240 321 266
Отношение справедливой бисимуляции (fair bisimulation)      239
Отношение справедливой симуляции (fair simulation)      244 254
Отношение тотальное (total)      57
Отношение цельное (monolithic)      119
Отрицание (negation)      90
Оценка (Valuation)      39 102
Перебор исчерпывающий (Exhaustive exploration)      23
Переменная булева (boolean)      50
Переменная общая, разделяемая (shared variable)      43 50
Переменная пропозициональная (prepositional)      102
Переменная реляционная (relational)      143
Переменная свободная (free)      143
Переменная связанная (bounded)      143
Переменная следующего состояния (next state)      40
Переменная текущего состояния (present state)      40
Переменная часов (clock)      345
Пересечение автоматов (of automata)      178
Пересечение, матрицы разностных границ (of difference bound matrices)      368
Пересечение, часовые пояса (of clock zones)      362
Перестановка, в теории групп (Permutation, in group theory)      287
Перестановочность (Commutativity)      201
Переупорядочение динамическое (Dynamic reordering)      88
Переход (Transition)      37 143 197
Переход атомарный (atomic)      41
Переход видимый (visible)      203
Переход детерминированный (deterministic)      198
Переход допустимый (enabled)      198
Переход запрещённый (disabled)      198
Переход мгновенный (instantaneous)      344
Переход невидимый (invisible)      203
Переход недетерминированный (nondeterministic)      157
Переход по действию (action transition)      346
Переход по задержке (delay transition)      346
Планируемость (множества процессов) (Schedulability)      340
Поведение (Behaviour)      26 37
Подгруппа (subgroup)      286
Подгруппа, порожденная множеством элементов (generated by a set of elements)      287
Подслушивание (Snoop)      163
Подформула верхнего уровня (top-level)      145
Подформула максимальная (maximal)      80
Позиция (Location)      344 345
Поиск в глубину с возвратом (depth first search, DFS)      182
Поиск в ширину (breadth first search)      199 293
Полнота спецификации (Specification completeness)      26
Пороговая секция (Trying region)      158
Последовательная программа (Sequential program)      45
Последовательность происшествий (eventuality sequence)      74
Последовательность чередования (interleaving sequence)      32
Пояс часовой (Clock zone)      361
Правило вывода (inference rule)      253
Правило инварианта (invariant rule)      306
Правило порождающее (production rule)      313
Правило преобразований (transformation rules)      87
Предикат (predicate)      96
Предохранитель (guard)      228 344
Предохранитель открытый (passable)      228
Представители (Representatives)      197
Представление моделей Крипке неявное (implicite)      29
Представление моделей Крипке первого порядка (first-order)      39
Представление моделей Крипке явное (explicite)      64
Преобразователь предикатов (Predicate transformer)      29 96
Преобразователь предикатов монотонный (monotonic)      96
Преобразователь предикатов непрерывный (continuous)      96
Проблема достижимости reachability problem      344 346
Проблема изоморфизма графов (graph isimorphism problem)      296
Проблема орбит (orbit problem)      296
Проверка на модели (Model checking)      21 24
Проверка на модели на представительной модели (using representatives)      197
Проверка на модели с использованием автоматов (Model checking using automata)      174
Проверка на модели «на лету» (on-the-fiy)      193
Проверка пустоты автомата Бюхи (Emptiness checking of Buchi automata)      182
Программы параллельные (concurrent)      49
Программы последовательные (sequential)      46
Продукция (Production rule)      313
Прореживание (Stuttering)      203
Пространство состояний (state space)      21 24 29 34
Протокол защиты (security protocol)      23
Протокол когерентности кэш-памяти (cache coherence protocol)      162 301 308
Протокол кольца с маркером (token ring protocol)      298
Протокол коммуникационный (communication protocol)      37
Протокол синхронной взаимосвязи (handshaking protocol)      43
Протокол шины (bus protocol)      163
Проход автомата (Run of automaton)      172
Проход автомата допускающий (accepting)      173 174
Процесс (process)      49 228
Процесс активный (active)      228
Процесс апериодический (aperiodic)      338
Процесс инвариантный (invariant)      36
Процесс пассивный (passive)      228
Процесс периодический (periodic)      338
Путь (path)      38 57 198
Путь справедливый (fair)      62 239 255
Разложение Шеннона (Shannon expansion)      89
Разметка вершин (node labeling)      64 311
Разметка программы (labeling transformations)      46
Разметка рёбер (edge labeling)      311
Расщепление дизъюнктивное (disjunctive)      120
Расщепление конъюнктивное (conjunctive)      120
Редукция на лету (on-the-fly)      199
Редукция по конусу влияния (cone of influence reduction)      262
Редукция частичных порядков (partial order reduction)      32 197
Реляционное произведение (Relational product)      103
Рубеж (Frontier)      334
Сборка мусора (garbage collection)      192

Свидетельства, подтверждающие вычисления (Witnesses)      109
Связки булевы (Connectives)      55
Секция критическая (critical)      52 158
Секция некритическая (noncritical)      52 158
Семантика временных автоматов (timed automata semantics)      345
Семантика логики CTL*      57
Семантика справедливая (fair)      62
Семантика чередования (interleaving semantics)      45
Сильно связная компонента (Strongly connected component, SCC)      66
Сильно связная компонента нетривиальная (nontrivial)      66
Сильно связная компонента самодостаточная (self-fulfilling)      76
Сильно связная компонента справедливая (fair)      70
Символьная верификация моделей (Symbolic model checking)      95
Символьная верификация моделей для CTL      95 103
Символьная верификация моделей для LTL      128
Симметрия (symmetry)      35 286 293
Симуляция (Simulation)      240
Симуляция наибольшая (largest)      247
Симуляция справедливая (fair)      251 254
Синхронизация процессов (Process synchronization)      50
Система SPIN (SPIN system)      227
Система абстрактная (abstract)      35
Система аппаратная (hardware)      21
Система верификации, верификатор (verification system)      21 30 61
Система встроенная (embedded)      22
Система ключевая (critical)      23
Система параллельная (concurrent systems)      23 38
Система переходов (transition system)      198 158
Система построения доказательств (proof system)      24
Система программная (software)      21
Система реагирующая (reactive)      37 55
Система реального времени (real-time systems)      327
Система реального времени, дискретная (discrete real-time systems)      329
Система с бесконечным числом состояний (infinite state system)      24
Система с конечным числом состояний, конечная (finite state system)      21 24
Слово бесконечное (infinite)      174
Слово входное (input)      173
Слово конечное (finite)      173
Слово пустое (empty)      173
События (events)      25
События независимые (independent)      32
События параллельные (concurrent)      32 198
События частично упорядоченные (partial ordered)      32
Состояние (state)      37 39
Состояние автомата (of automaton)      172
Состояние бисимуляционно эквивалентное (bisimulation equivalent)      237
Состояние вполне раскрытое (fully expanded)      205
Состояние допускающее (accepting)      174
Состояние заключительное (final)      172
Состояние начальное (initial)      39 56 64 172 346
Состояние освобождённое (invalid)      164
Сохранение, строгое и слабое (Preservation, strong and weak)      306
Спецификация (specification)      24 26 55
Справедливость (Fairness)      27 45 61
Статическое квантование времени (Static time-slicing)      327
Строка, как последовательность переходов (String, as sequence of transitions)      221
Структура времени ветвящаяся (branching)      27
Структура времени дискретная (discrete)      343
Структура времени линейная (linear)      27
Структура времени непрерывная (real-time)      343
Стягивание (Tightening)      368
Сужение модели (restriction of a model)      293
Сужение последовательности (restriction)      131
Суффикс (suffix)      58
Схема вывода «допущение-подтверждение» (Assume-guarantee reasoning)      257
Схема цифровая электронная (Digital circuits)      23 43
Счетчик команд (Program counter)      47 216
Таблица (Tableau)      254
Табличная конструкция (Tableau construction)      73
Табличная конструкция для ACTL (for ACTL)      247
Табличная конструкция для LTL (for LTL)      73 128
Табличная конструкция при композиционных рассуждениях (under compositional reasoning)      254
Теория групп (Group theory)      286
Тестирование (testing)      22
Точка входа в оператор (entry point)      46
Точка выхода из оператора (exit point)      46
Транзакция (transaction)      163
Транзакция разделяемая (split transaction)      163
Трансляция $\mu$ -исчисления в OBDD (of $\mu$ -calculus into OBDDs)      152
Трансляция CTL в $\mu$ -исчисление (of CTL into $\mu$ -calculus)      154
Трансляция LTL в автоматы (of LTL into automata)      186
Транспозиция (transposition)      287
Трасса ошибочная (Error trace)      26
Умножение, в группе (Group multiplication)      286
Универсальные кванторы пути (Universal path quantifiers)      61
Универсум (universe)      39
Условие (condition)      160 336
Условие булево (boolean)      47 50
Фактор-модель (Quotient models)      290
Флаг (flag)      183
Формула $\mu$ -исчисления ( $\mu$ -calculus formula)      143
Формула булева (boolean)      29 43 95
Формула булева, квантифицированная (quantified boolean)      102
Формула замкнутая (closed formula)      143
Формула инвариантная относительно прореживания (invariant under stuttering)      203
Формула пути (path formula)      57
Формула пути, ограниченная (restricted path formula)      128
Формула синтаксически монотонная (syntactically monotone)      143
Формула состояний (state formula)      57
Формула элементарная (elementary formula)      130 248
Функция абстракции (abstraction function)      269
Функция булева (boolean)      83 85
Функция характеристическая (characteristic function)      91
Цикл, в теории групп (Cycle, in group theory)      287
Часы (Clocks)      344
Эквивалентность автоматов (automata equivalence)      180
Эквивалентность бисимуляционная (bisimulation equivalence)      234 274 305 359 360
Эквивалентность моделей (equivalent structures)      244
Эквивалентность по прореживанию (stuttering equivalence)      203 204
Язык автомата (of an automaton)      173
Язык графовый (graph language)      313
Язык модели (of a structure)      174 244

1 2

О проекте