Принципы проверки модели
 Передняя обложка | |
| Автор | Кристель Байер и Йост-Питер Катоен |
|---|---|
| Предмет | Проверка модели |
| Издатель | С Прессой |
Дата публикации | 25 апреля 2008 г. |
| Страницы | 975 |
| ISBN | 9780262026499 |
«Принципы проверки моделей» — учебник по проверке моделей , области информатики , автоматизирующей задачу определения соответствия машины требованиям спецификации. Он был написан Кристель Байер и Йост-Питер Катоен и опубликован в 2008 году издательством MIT Press .
Краткое содержание
[ редактировать ]
Во введении и первой главе описывается область проверки модели : модель машины или процесса можно проанализировать, чтобы увидеть, сохраняются ли желаемые свойства. Например, торговый автомат может удовлетворять свойству «баланс никогда не может упасть ниже 0,00 евро». Видеоигра может применять правило: «Если у игрока 0 жизней, игра заканчивается проигрышем». И торговый автомат, и видеоигра могут быть смоделированы как переходные системы . Проверка модели — это процесс описания таких требований на математическом языке и автоматизации доказательства того, что модель удовлетворяет требованиям, или обнаружения контрпримеров , если модель ошибочна.
Вторая глава посвящена созданию подходящей модели для параллельных систем , в которой несколько частей алгоритма ( набора инструкций) могут выполняться одновременно разными машинами или частями машины.
В главе 3 рассматриваются типы правил, которым может удовлетворять система перехода: свойства линейного времени . Свойство безопасности , такое как «невозможны тупиковые состояния», имеет форму «нежелательный результат никогда не может произойти». Свойство жизнеспособности , такое как «общий ресурс всегда в конечном итоге будет доступен компоненту, который его запрашивает», имеет форму «желаемый результат в конечном итоге произойдет». Свойства справедливости, такие как «светофор никогда не перестает менять цвет», могут использоваться в качестве предварительных условий, т.е. предположений, из которых можно вывести другие свойства.
Четвертая глава посвящена регулярным и ω-регулярным свойствам языков, а также теоретическим машинам, таким как автоматы Бюхи , которые моделируют языки. Он предоставляет алгоритмы проверки моделей для проверки свойств или поиска контрпримеров.
В пятой и шестой главах рассматриваются линейная временная логика (LTL) и логика дерева вычислений (CTL), два класса формул, выражающих свойства. LTL кодирует требования к путям в системе, например: «каждый игрок в «Монополию» бесконечно часто передает «Go»; CTL кодирует требования к состояниям в системе, например, «из любой позиции все игроки в конечном итоге могут попасть на «Go»». Также определены формулы CTL* , объединяющие две грамматики. Приведены алгоритмы формул проверки моделей в этих логиках.
В седьмой главе исследуются формальные способы сравнения переходных систем, такие как бисимуляция ; восьмой касается частичного понижения порядка , целью которого является сокращение объема вычислений, необходимых для проверки свойств модели. Девятая и десятая главы посвящены расширениям ранее рассмотренных логик и автоматов, в том числе за счет добавления тактовой частоты ( автоматы с таймером ) или вероятностей ( вероятностные автоматы , основанные на цепях Маркова ).
Прием
[ редактировать ]Франсуа Ларуссини в статье для The Computer Journal рекомендовал книгу исследователям, преподавателям, студентам и инженерам, назвав книгу «впечатляющей». Ларуссини нашел учебник всеобъемлющим и доступным, с большим количеством примеров, упражнений и мотивирующих идей по ключевым понятиям. В рамках «унифицированной структуры» первые семь глав посвящены классической теории, а последние три главы посвящены расширению проверки моделей. [1]
В обзорах ACM Computing Reviews Габриэль Чобану высказал мнение, что учебник можно использовать на курсах повышения квалификации студентов и аспирантов, а также он будет полезен исследователям. Чобану похвалил «ясную и интуитивно понятную» презентацию и сказал, что ее «следует ценить за педагогический подход к освещению основных концепций, глубоких теоретических результатов и сложных тем в исследованиях по проверке моделей». [2]
В 2014 году книга вошла в пятерку самых цитируемых научных текстов, отслеживаемых Индексом цитирования книг (BKCI). [3]
Ссылки
[ редактировать ]- ^ Ларуссини, Франсуа (2010). «Принципы проверки моделей (обзор)». Компьютерный журнал . 53 (5): 615–616. дои : 10.1093/comjnl/bxp025 .
- ^ Чобану, Габриэль (8 января 2009 г.). «Принципы проверки моделей (обзор)» . Обзоры вычислений ACM .
- ^ Куша, Кайван; Телвалл, Майк (1 марта 2016 г.). «Могут ли обзоры Amazon.com помочь оценить более широкое влияние книг?». Журнал Ассоциации информационных наук и технологий : 580.
Дальнейшее чтение
[ редактировать ]- Ланге, Мартин (2010), MathSciNet , MR 2493187
{{citation}}: CS1 maint: периодическое издание без названия ( ссылка )