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

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

Авторизация

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

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

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

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

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

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

Аннотация:

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

Язык:

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

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

ed2k: ed2k stats

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

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

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

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

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

$LTL_{-X}$ Темпоральная логика линейного времени без оператора сдвига по времени (nexttime)      204 205
$\mu$ -исчисление ( $\mu$ -calculus)      141
ACTL (Универсальная CTL)      61 244 247 254 265
ACTL справедливая (fair ACTL)      254
ACTL* (Универсальная ACTL*)      61 242 244 268 274 305
CTL*, (Обобщенная логика деревьев вычислений)      56 79 239 265 274 292 306
CTL, (Computation Tree Logic, Логика деревьев вычислений)      59 64 102 154 157 234
DFS (Depth First Search, Поиск в глубину с возвратом)      182
Futurebus+      162
ICTL* (Индексированная CTL*)      304
LTL (Linear Temporal Logic, Темпоральная логика линейного времени)      59 72 32 128 186 227
OBDD (Ordered Binary Decision Diagram, Упорядоченная двоичная разрешающая диаграмма)      29 83 85 87 102 117 128 152 282 294
PROMELA (PROMELA language)      227
PSPACE-полнота (PSPACE-completeness)      195
RMS (Rate-Monotonic Scheduling, Монотонное расписание)      328
RTCTL (логика CTL реального времени)      331
SMV (Symbolic Model Verifier, Символьный верификатор моделей)      157
Spin      227
Абстракция (abstraction)      35 240 262 265
Абстракция данных (data abstraction)      262 265
Абстракция декартова произведения (product abstraction)      281
Абстракция модели (of a structure)      240
Абстракция одиночного бита (single bit abstraction)      281
Абстракция символьная (symbolic)      282
Абстракция состояния (of a state)      320
Абстракция экзистенциальная (existential)      269
Автомат Бюхи (Buchi automata)      174
Автомат Бюхи, обобщённый (Generalized Buchi automata)      181
Автомат временной (Timed automaton)      344 345
Автомат детерминированный (deterministic)      180
Автомат над бесконечными словами, (automaton over infinite words)      172
Автомат недетерминированный (nondeterministic)      180
Автомат, $\omega$ -автомат ( $\omega$ -automaton)      172
Автомат, включение языков (Language containment)      195
Автомат, пересечение и дополнение (intersection and complementation)      178
Автомат, проверка пустоты (emptiness checking)      182
Автоморфизм (automorphism)      287
Алгоритм Apply (Apply algorithm)      89
Алгоритм анализа достижимости (reachability algorithm)      293
Алгоритм верификации моделей для $\mu$ -исчисления (model checking algorithm for the $\mu$ -calculus)      146
Алгоритм верификации моделей для CTL (CTL model checking algorithm)      64
Алгоритм верификации моделей для CTL* (CTL* model checking algorithm)      79
Алгоритм верификации моделей для LTL (LTL model checking algorithm)      72 220
Алгоритм выбора лидера (leader election algorithm)      228
Алгоритм вычисления максимальной задержки (maximum delay algorithm)      333
Алгоритм вычисления минимальной задержки (minimum delay algorithm)      332
Алгоритм вычисления наибольшей бисимуляции (for computing the largest bisimulation)      245
Алгоритм вычисления пересечения (for computing intersection)      180
Алгоритм глобальный (global)      141
Алгоритм двойного поиска в глубину с возвратом, DFS (double depth first search algorithm)      182
Алгоритм жадный (greedy)      124
Алгоритм квазипорядка (preorder algorithm)      244
Алгоритм количественного анализа (quantitative algorithm)      336
Алгоритм кольца с маркерами (token-ring algorithm)      288
Алгоритм Лихтенштейн — Пнуели (Lichtenstein — Pnueli algorithm)      77
Алгоритм локальный (local)      141
Алгоритм подсчета условий (condition counting algorithm)      336
Алгоритм поиска в глубину с редукцией частичных порядков (depth-first search with partial order reduction)      200
Алгоритм символьная верификация моделей для CTL (CTL symbolic model checking algorithm)      103
Алгоритм символьной верификации моделей для LTL (LTL symbolic model checking algorithm)      128
Алгоритм Тарьяна поиска в глубину с возвратом (Tarjan depth first search algorithm)      182
Алгоритм трансляции LTL в автоматы (for translating LTL into automata)      186
Алгоритм Флойда — Уоршалла (Floyd — Warshall algorithm)      368
Алгоритм эквивалентности (equivalence algorithm)      244
Алгоритм Эмерсона — Ли (Emerson and Lei algorithm)      151
Алфавит (alphabet)      172 345
Алфавит вершин (Node alphabet)      311
Алфавит нетерминальных вершин (Nonterminal node alphabet)      313
Алфавит рёбер (Edge alphabet)      311
Алфавит терминальных вершин (Nonterminal node alphabet)      313
Анализ дедуктивный (Deductive verification)      23
Анализ количественный временной (quantitative temporal)      327
Аппроксимация (approximation)      269
Аппроксимация вычисление (approximations, computing)      269
Аппроксимация неподвижной точки (fixpoint approximation)      146
Аппроксимация точная (exact)      274
Архитектура шины (Bus architecture)      163
Асинхронное выполнение (Asynchronous execution)      43
Асинхронные системы (Asynchronous systems)      32 343
Атом (atom)      73
Аттрибут булев (Boolean attribute)      166
Бесконечные семейства грамматик, графовых и сетевых (grammars, graph and network)      311
Бесконечные семейства систем с конечным числом состояний (finite-state systems)      304 345 346 359
Бесконечные слова (Infinite words)      174
Бисимуляция (Bisimulation)      234 265
Бисимуляция наибольшая (largest)      244
Бисимуляция справедливая (fair)      239
Бисимуляция фактор-модели (of the quotient model)      292
Блок (block)      203 298
Блокировать (To block)      228 336
Булевы аттрибуты (attributes)      166
Булевы вектора (vector)      91 152
Булевы значения (values)      29 37
Булевы константы (constants)      190
Булевы кортежи (arrays)      356
Булевы отношения (relations)      91 103 158
Булевы переменные (variables)      50
Булевы связки (connectives)      55 152
Булевы тождества (equivalences)      186
Булевы условия (conditions)      47
Булевы флаги (flags)      183
Булевы формулы (formulas)      29 43 95 102
Булевы формулы, квантифицированные (quantified boolean formulas)      102
Булевы функции (functions)      83 85
Верификация (verification)      21 26
Верификация аппаратуры и программного обеспечения (of hardware and software)      21
Верификация асинхронных программных систем (of asynchronous software systems)      227
Верификация вероятностная (probabilistic)      376
Верификация комбинационных логических схем (of combinational logic)      83
Верификация композиционная (compositional)      252
Верификация моделей (Model checking)      24 64
Верификация моделей для $\mu$ -исчисления (model checking for the $\mu$ -calculus)      146 155
Верификация моделей для CTL (CTL model checking)      64 102
Верификация моделей для CTL* (CTL* model checking)      79
Верификация моделей для LTL, табличная (LTL model checking by tableau)      72 128
Верификация моделей для RTCTL (RTCTL model checking)      331
Верификация моделей при помощи автоматов (using automata)      174
Верификация моделей символьная symbolic verification      95
Верификация моделей «на лету» (on-the-fly model checking)      193 199
Верификация параллельных систем (of concurrent systems)      21
Верификация систем реального времени (real-time system verification)      329
Верификация систем с конечным числом состояний (of finite state systems)      24
Вершина, узел в алгоритме трансляции LTL в автоматы (node)      187
Вершина, узел в двоичных разрешающих деревьях (vertex, in binary decision trees)      85
Вершина, узел, внутренняя (nonterminal vertex)      85
Вершина, узел, входная (input node)      313
Вершина, узел, выходная (output node)      313
Вершина, узел, нетерминальная (nonterminal)      84
Вершина, узел, помеченная (flagged node)      183
Вершина, узел, терминальная (terminal)      84
Вершина, узел, хэшированная (hashed node)      183
Взаимная блокировка (Deadlock)      171 227
Взаимное исключение (Mutual exclusion)      50
Временной анализ, количественный (Temporal analysis, quantitative)      332
Встроенные системы (Embedded systems)      22
Вход в критическую секцию (Trying region)      52
Выражение, регулярное (Regular expression)      173
Высказывание атомарное (atomic)      38 40
Вычисление (computation)      37
Вычислимость, теория вычислимости (Computability, theory of)      23
Глубина чередований (Alternation depth)      142 145
Грамматики (grammars)      313
Грамматики, грамматики (graph grammars)      313
Грамматики, контекстно-свободная графовая (context-free graph grammar)      313
Грамматики, сетевая (network grammar)      313
Гранулярность (Granularity)      41
Граф (graph)      1
Граф областей (region graph)      359
Граф переходов (state graph)      38 56
Граф переходов, сокращённый (reduced state graph)      199

Граф часовых поясов (zone graph)      364
Граф, ориентированный ациклический граф (directed acyclic graph)      85
Группа (group)      286
Группа автоморфизмов (automorphysm group)      288
Группа вращений (rotation groups)      298
Группа инвариантности (invariance group)      290
Группа перестановок (permutation group)      287
Группа полная симметрическая (full symmetric group)      287 298
Дерево вычислений (computation)      56
Дерево двоичное разрешающее (binary decision)      83
Диаграмма временная (timing)      373
Диаграмма двоичная разрешающая (binary decision (BDDs))      29 83 85
Диаграмма упорядоченная двоичная разрешающая (ordered binary decision, OBDDs)      29 83
Диаграмма, изоморфная (isomorphic)      85
Длина пути (Length, of a path)      332
Доказательство правильности программы (Deductive verification)      23
Домен (Domain)      39
Дополнение (Complementation)      178
Допущение-подтверждение (Assume-guarantee)      35 252
Достаточные множества (Ample sets)      34
Достижимости задача (Reachability problem)      214 346
Дуга возврата (Back edge)      215
Единичный элемент (Identity)      286
Задача верификации моделей (model checking problem)      64
Задача об изоморфизме графов (graph isomorphism problem)      296
Задача орбит (orbit problem)      296
Замыкание множества элементов группы (of a set of elements)      287
Замыкание формулы (of a formula)      73
Захват данных (Snarfling)      164
Значение абстрактное (abstract)      266
Значение неопределённое (undefined)      47
Инвариант (invariant)      23 290
Инвариант бесконечного семейства моделей (for infinite family of structures)      305
Инвариант дислокации (of the location)      344 345
Инверсия приоритетов (Priority inversion)      336
Индукция (induction)      36
Интерпретация часов (Clock interpretation)      346
Исключающее ИЛИ (exclusive OR)      45
Истощение (удушение) (Starvatiuon)      54
Каноническое представление (Canonical representation)      83 85
Квазипорядок симуляции (Simulation preorder)      240 305
Квантование времени, статическое (Time-slicing, static)      327
Кванторы пути (Path quantifiers)      56
Кеш результатов (Result cache)      90
Кеш-строка (cache line)      163
Китайская теорема об остатках (Chinese remainder theorem)      278
Кольцо с маркерами (Token ring)      288 306 322
Комбинаторный взрыв в пространстве состояний (State explosion)      21 34
Коммутативность, перестановочность (Commutativity)      201
Композиционные доказательства (Compositional reasoning)      252
Композиция абстрактная (abstract)      321
Композиция интерливинговая (interleaving)      157
Композиция параллельная (parallel)      255 347
Композиция последовательная (sequential)      49
Композиция синхронная (synchronous)      157
Компонент (Component)      35
Конгруентность (Congruence)      274
Контрпример (Counterexample)      26 109 178
Конус влияния (Influence cone)      262
Логика деревьев вычислений (Computation Tree Logic)      56 59
Логика линейного времени (Linear Temporal Logic, LTL)      59
Логика темпоральная (temporal)      26 55
Ложное опровержение (False negative trace)      26
Маркер (Token)      324
Матрица разностных границ (Difference bound matrix)      363 367
Машина Мура (Moore machine)      276
Машина Тьюринга (Turing machine)      322
Мера стоимости (Cost metrics)      124
Метка (label)      46 47
Метка начальная (Start label)      313
Метод абстракции (abstraction technique)      265
Метод верификации моделей (model checking algorithm)      64 95 172
Метод имитационного моделирования (simulation technique)      23
Метод индукции (induction technique)      308
Метод подмножеств (subset construction)      180
Метод представления модели Крипке (Kripke structure encoding)      91
Метод развертки (unfolding technique)      34
Микроволновая печь, пример (Microwave oven example)      68
Множество выпуклое (convex set)      345
Множество достаточное (ample)      34 205
Множество оцепеневшее (sleep)      34
Множество упорное (stubborn)      34
Множество устойчивое (persistent)      34
Моделирование имитационное (Simulation)      22
Модель вычислений формальная (formal)      37
Модель вычислений частичного порядка (partial order)      32
Модель вычислений чередования (interleaving)      32
Модель Крипке (Kripke structure)      27 38
Модель Крипке бисимуляционно эквивалентная (bisimulation equivalent)      234 239
Модель Крипке бисимуляционно эквивалентная в справедливом смысле (fair bisimulation equivalent)      239
Модель Крипке в $\mu$ -исчислении ( $\mu$ -calculus modification)      143
Модель Крипке детерминированная (deterministic)      244
Модель Крипке максимальная (maximal)      247
Модель Крипке недетерминированная (nondeterministic)      244
Модель Крипке справедливая (fair)      254 62
Модуль, в SMV (Module, in SMV)      157
Модульная структура (Modular structure)      34
Монитор (Monitor)      337
Монотонное расписание (Rate-monotonic scheduling (RMS))      328
Монотонности условие (Monotonicity condition)      315
Монотонность (Monotonicity)      96
Монотонность композиции (of composition)      306
Монотонность синтаксическая (syntactic)      143
Мост, между шинами (Bus bridge)      163
Невидимость (Invisibility)      201
Неподвижная точка (fixpoint)      95 96
Неподвижная точка в $\mu$ -исчисление ( $\mu$ -calculus)      143
Неподвижная точка наибольшая (the greatest fixpoint)      96
Неподвижная точка наименьшая (the least fixpoint)      96
Непрерывное реальное время (Continuous real time)      343
Неразрешимость (undecidability)      36 322
Нормальная форма (normal form)      83
Нормальная форма дизъюнктивная (disjunctive)      83
Нормальная форма конъюнктивная (conjunctive)      83
Нормальная форма негативная (negative)      61 186
Область абстрактных значений (domain of abstract values)      266
Область действия квантора (scope of quantification)      121
Область значений переменной (domain, Universe)      265
Область конечная (finite)      91
Область определения прохода (domain of a run)      174
Область часовая (clock regions)      353 355
Обмен сообщениями (Message exchange)      43
Обратный элемент (Inverse element)      286
Ограничение временное (timing constraint, clock constraint)      331 336 344 345
Ограничение справедливости (fairness constraints)      62 70
Окружение (environment)      143
Оператор абстракции (abstraction operator)      269
Оператор неподвижной точки (fixpoint operator)      141 143
Оператор программы If-then-else (If-then-else statement)      49
Оператор программы Lock (Lock statement)      52
Оператор программы Skip (Skip statement)      47
Оператор программы Unlock (Unlock statement)      52
Оператор программы Wait (Wait statement)      50
Оператор программы While (While statement)      49
Оператор программы ожидания по условию (Busy waiting statement)      50
Оператор программы присваивания (Assignment statement)      47
Оператор программы размеченный (labelled statement)      46
Оператор темпоральный (Temporal operator)      56
Оператор темпоральный инвариантности (globally, G)      57
Оператор темпоральный ожидания (until, U)      57
Оператор темпоральный ожидания, ограниченный (bounded until)      331
Оператор темпоральный происшествия (eventually, F)      56
Оператор темпоральный разблокировки (release, R)      57
Оператор темпоральный сдвига по времени (next time, X)      56
Операция логическая (logical)      88 89
Операция сброса часов (clock reset operation)      362
Орбита (orbit)      290
Отказ, вероятность отказа (Failure, probability of)      21
Отношение бисимуляции (bisimulation)      234 239
Отношение булево (boolean)      91 103 158

1 2

О проекте