Проверка модели

Область информатики

Программное обеспечение управления лифтом можно проверить на модели, чтобы проверить как свойства безопасности, такие как «Кабина никогда не движется с открытой дверью» ^[1] , так и свойства работоспособности, такие как «Каждый раз, когда нажимается кнопка вызова на n- ^м этаже , кабина в конечном итоге останавливается». на n-м ^этаже и откройте дверь» .

В информатике проверка модели или проверка свойств — это метод проверки того, соответствует ли модель конечного состояния системы заданной спецификации (также известной как корректность ). Обычно это связано с аппаратными или программными системами , где спецификация содержит требования к работоспособности (например, предотвращение блокировки в реальном времени ), а также требования безопасности (например, предотвращение состояний, представляющих сбой системы ).

Для алгоритмического решения такой задачи и модель системы, и ее спецификация формулируются на каком-то точном математическом языке. Для этого задача формулируется как задача по логике , а именно проверить, удовлетворяет ли структура заданной логической формуле. Эта общая концепция применима ко многим видам логики и многим видам структур. Простая задача проверки модели состоит в проверке того, удовлетворяет ли формула логики высказываний данной структуре.

Обзор

Проверка свойств используется для проверки , когда два описания не эквивалентны. В ходе доработки спецификация дополняется деталями, ненужными в спецификации более высокого уровня. Нет необходимости проверять вновь введенные свойства на соответствие исходной спецификации, поскольку это невозможно. Таким образом, строгая двунаправленная проверка эквивалентности заменена односторонней проверкой свойств. Реализация или проект рассматривается как модель системы, тогда как спецификации — это свойства, которым должна удовлетворять модель. ^[2]

Важный класс методов проверки моделей был разработан для проверки моделей аппаратных и программных средств , спецификация которых задается формулой временной логики . Новаторскую работу в области спецификации темпоральной логики провел Амир Пнуэли , получивший в 1996 году премию Тьюринга за «новаторскую работу по внедрению темпоральной логики в информатику». ^[3] Проверка моделей началась с новаторских работ Э.М. Кларка , Э.А. Эмерсона , ^{[4] [5] [6]} Дж. П. Квейля и Дж. Сифакиса . ^[7] Кларк, Эмерсон и Сифакис получили премию Тьюринга 2007 года за плодотворную работу по созданию и развитию области проверки моделей. ^{[8] [9]}

Проверка модели чаще всего применяется к проектам аппаратного обеспечения. Для программного обеспечения из-за неразрешимости (см. теорию вычислимости ) подход не может быть полностью алгоритмическим, применяться ко всем системам и всегда давать ответ; в общем случае оно может не доказать или не опровергнуть данное свойство. Во встроенных системах можно проверить достоверность предоставленной спецификации, например, с помощью диаграмм деятельности UML ^[10] или интерпретируемых с помощью управления сетей Петри . ^[11]

Структура обычно задается в виде описания исходного кода на языке описания промышленного оборудования или языке специального назначения. Такая программа соответствует конечному автомату (КАМ), т. е. ориентированному графу, состоящему из узлов (или вершин ) и ребер . С каждым узлом связан набор атомарных предложений, обычно указывающих, какие элементы памяти являются одним из них. Узлы представляют состояния системы, ребра представляют собой возможные переходы, которые могут изменить состояние , а атомарные предложения представляют собой основные свойства, которые сохраняются в момент выполнения.

Формально задачу можно сформулировать следующим образом: учитывая желаемое свойство, выраженное в виде формулы темпоральной логики , и структуру с начальным состоянием , решить, если . Если конечно, как и в аппаратном обеспечении, проверка модели сводится к поиску по графу . ${\displaystyle p}$ ${\displaystyle M}$ ${\displaystyle s}$ ${\displaystyle M,s\models p}$ ${\displaystyle M}$

Символьная проверка модели

Вместо перечисления достижимых состояний по одному, пространство состояний иногда можно обойти более эффективно, рассматривая большое количество состояний за один шаг. Когда такой обход пространства состояний основан на представлении набора состояний и отношений перехода в виде логических формул, бинарных диаграмм решений (BDD) или других связанных структур данных, метод проверки модели является символическим .

Исторически первые символьные методы использовали BDD . После успеха пропозициональной выполнимости при решении задачи планирования в искусственном интеллекте (см. satplan ) в 1996 году тот же подход был обобщен для проверки модели на линейную временную логику (LTL): задача планирования соответствует проверке модели на свойства безопасности. Этот метод известен как ограниченная проверка модели. ^[12] Успех решателей логической выполнимости в ограниченной проверке моделей привел к широкому использованию решателей выполнимости в символьной проверке модели. ^[13]

Пример

Один из примеров такого системного требования: между моментом вызова лифта на этаже и моментом открытия дверей на этом этаже лифт может прибыть на этот этаж не более двух раз . Авторы книги «Шаблоны в спецификации свойств для проверки конечных состояний» переводят это требование в следующую формулу LTL: ^[14]

Не удалось проанализировать (SVG (MathML можно включить через плагин браузера): неверный ответ («Расширение Math не может подключиться к Restbase.») с сервера «http://localhost:6011/en.wikipedia.org/v1/»:) : {\displaystyle \begin{align}\Box\Big((\texttt{call} \land \Diamond \texttt{open}) \to & \big((\lnot \texttt{atfloor} \land \lnot \texttt {open}) ~\mathcal{U} \\ & (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U}\\ & (\texttt {open} \lor ((\lnot \texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\ & (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\ & (\texttt{open} \lor (\lnot \texttt{atfloor} ~\mathcal{U}~ \texttt{open}))))) )))\big)\Big)\end{align}}

Здесь следует читать как «всегда», «в конце концов», как «пока», а остальные символы являются стандартными логическими символами, «или», «и» и «нет». ${\displaystyle \Box }$ ${\displaystyle \Diamond }$ ${\displaystyle {\mathcal {U}}}$ ${\displaystyle \lor }$ ${\displaystyle \land }$ ${\displaystyle \lnot }$

Техники

Инструменты проверки моделей сталкиваются с комбинаторным разрушением пространства состояний, широко известным как проблема взрыва состояний , которую необходимо решать для решения большинства реальных проблем. Существует несколько подходов к борьбе с этой проблемой.

1. Символьные алгоритмы избегают явного построения графа для конечных автоматов (FSM); вместо этого они представляют график неявно, используя формулу количественной логики высказываний. Использование диаграмм двоичных решений (BDD) стало популярным благодаря работе Кена Макмиллана ^[15] и разработке библиотек манипуляции BDD с открытым исходным кодом, таких как CUDD ^[16] и BuDDy. ^[17]
2. Алгоритмы проверки ограниченной модели разворачивают автомат на фиксированное количество шагов и проверяют, может ли нарушение свойства произойти за меньшее количество шагов. Обычно это предполагает кодирование ограниченной модели как экземпляра SAT . Процесс можно повторять со все большими и большими значениями до тех пор, пока не будут исключены все возможные нарушения (см. Итеративный поиск в глубину с углублением ). ${\displaystyle k}$ ${\displaystyle k}$ ${\displaystyle k}$
3. Абстракция пытается доказать свойства системы, сначала упрощая ее. Упрощенная система обычно не обладает теми же свойствами, что и исходная, поэтому может потребоваться процесс ее усовершенствования. Как правило, требуется, чтобы абстракция была обоснованной (свойства, доказанные в абстракции, верны для исходной системы); однако иногда абстракция не является полной (не все истинные свойства исходной системы верны и для абстракции). Примером абстракции является игнорирование значений небулевых переменных и рассмотрение только логических переменных и потока управления программой; такая абстракция, хотя она и может показаться грубой, на самом деле может быть достаточной, чтобы доказать, например, свойства взаимного исключения .
4. Уточнение абстракции на основе контрпримеров (CEGAR) начинает проверку с грубой (то есть неточной) абстракции и итеративно уточняет ее. Когда обнаруживается нарушение (т. е. контрпример ), инструмент анализирует его на предмет осуществимости (т. е. является ли нарушение подлинным или является результатом неполной абстракции?). Если нарушение допустимо, об этом сообщается пользователю. Если это не так, доказательство невыполнимости используется для уточнения абстракции и проверка начинается заново. ^[18]

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

Логика первого порядка

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

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

Эта проблема находится в схеме класса AC 0 . Его можно использовать при наложении некоторых ограничений на входную структуру: например, требуя, чтобы ширина дерева была ограничена константой (что в более общем смысле подразумевает удобство проверки модели для монадической логики второго порядка ), ограничивая степень каждого элемента предметной области, и более общие условия, такие как ограниченное расширение , локально ограниченное расширение и нигде не плотные структуры. ^[19] Эти результаты были распространены на задачу перечисления всех решений формулы первого порядка со свободными переменными. ^{[ нужна цитата ]}

Инструменты

Вот список важных инструментов проверки модели:

• Afra: средство проверки моделей для Rebeca , основанного на актерах языка для моделирования параллельных и реактивных систем.
• Сплав (анализатор сплавов)
• BLAST (инструмент проверки программного обеспечения для ленивой абстракции Беркли)
• CADP (построение и анализ распределенных процессов) набор инструментов для проектирования протоколов связи и распределенных систем.
• CPAchecker : средство проверки моделей программного обеспечения с открытым исходным кодом для программ C, основанное на платформе CPA.
• ECLAIR : платформа для автоматического анализа, проверки, тестирования и преобразования программ на C и C++.
• FDR2 : средство проверки моделей для проверки систем реального времени, смоделированных и заданных как процессы CSP .
• Верификатор уровня кода ISP для программ MPI
• Java Pathfinder : средство проверки моделей с открытым исходным кодом для программ Java.
• Libdmc : платформа для проверки распределенных моделей.
• Набор инструментов mCRL2 , лицензия на программное обеспечение Boost , на основе ACP
• NuSMV : новая программа проверки символьных моделей
• PAT : расширенный симулятор, средство проверки моделей и средство проверки уточнений для параллельных систем и систем реального времени.
• Prism : вероятностная программа проверки символьных моделей.
• Roméo : интегрированная инструментальная среда для моделирования, симуляции и проверки систем реального времени, моделируемых как параметрические, временные сети Петри и сети секундомера.
• SPIN : общий инструмент для проверки правильности моделей распределенного программного обеспечения строгим и в основном автоматизированным способом.
• Storm: ^[20] Средство проверки моделей вероятностных систем.
• TAPA : инструмент для анализа алгебры процессов
• TAPAAL : интегрированная инструментальная среда для моделирования, проверки и верификации сетей Петри с временной дугой.
• Средство проверки модели TLA+ от Лесли Лэмпорта
• UPPAAL : интегрированная инструментальная среда для моделирования, проверки и верификации систем реального времени, смоделированных как сети синхронизированных автоматов.
• Zing ^[21] — экспериментальный инструмент от Microsoft для проверки моделей состояния программного обеспечения на различных уровнях: высокоуровневые описания протоколов, спецификации рабочих процессов, веб-сервисы, драйверы устройств и протоколы в ядре операционной системы. В настоящее время Zing используется для разработки драйверов для Windows.

Смотрите также

• Абстрактная интерпретация
• Автоматизированное доказательство теорем
• Бинарная диаграмма решений
• Автомат Бючи
• Логика дерева вычислений
• Формальная проверка
• Линейная темпоральная логика
• Список инструментов проверки модели
• Частичное сокращение заказа
• Программный анализ (информатика)
• Статический анализ кода

Рекомендации

1. Для удобства примеры свойств перефразированы здесь на естественном языке. Средства проверки моделей требуют, чтобы они были выражены в некоторой формальной логике, например LTL .
2. Лам К., Уильям (2005). «Глава 1.1: Что такое проверка проекта?». Верификация проекта аппаратного обеспечения: подходы, основанные на моделировании и формальных методах . Проверено 12 декабря 2012 г.
3. "Амир Пнуэли - лауреат премии А. М. Тьюринга" .
4. Аллен Эмерсон, Э.; Кларк, Эдмунд М. (1980), «Характеристика свойств корректности параллельных программ с использованием фиксированных точек», Автоматы, языки и программирование , конспекты лекций по информатике, том. 85, стр. 169–181, doi : 10.1007/3-540-10003-2_69, ISBN. 978-3-540-10003-4
5. Эдмунд М. Кларк, Э. Аллен Эмерсон: «Проектирование и синтез скелетов синхронизации с использованием временной логики времени ветвления». Логика программ 1981: 52-71.
6. Кларк, EM; Эмерсон, Э.А.; Систла, AP (1986), «Автоматическая проверка параллельных систем с конечным состоянием с использованием спецификаций темпоральной логики», ACM Transactions on Programming Languages ​​and Systems , 8 (2): 244, doi : 10.1145/5397.5399 , S2CID  52853200
7. Кейль, JP; Сифакис, Дж. (1982), «Спецификация и проверка параллельных систем в CESAR», Международный симпозиум по программированию , Конспекты лекций по информатике, том. 137, стр. 337–351, doi : 10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9
8. «Пресс-релиз: Премия Тьюринга ACM вручается основателям технологии автоматической проверки» . Архивировано из оригинала 28 декабря 2008 г. Проверено 6 января 2009 г.
9. USACM: Объявлены лауреаты премии Тьюринга 2007 года
10. Гробельна, Ивона; Гробельный, Михал; Адамски, Мариан (2014). «Проверка модели диаграмм деятельности UML при проектировании логических контроллеров». Материалы Девятой международной конференции по надежности и сложным системам DepCoS-RELCOMEX. 30 июня – 4 июля 2014, Брунув, Польша . Достижения в области интеллектуальных систем и вычислений. Том. 286. стр. 233–242. дои : 10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.
11. И. Гробельна, «Формальная проверка спецификации встроенного логического контроллера с компьютерным выводом во временной логике», Przeglad Elektrotechniczny, Vol.87, выпуск 12a, стр. 47–50, 2011 г.
12. Кларк, Э.; Бьер, А.; Рэйми, Р.; Чжу, Ю. (2001). «Проверка ограниченной модели с использованием решения выполнимости». Формальные методы проектирования систем . 19 :7–34. дои : 10.1023/А: 1011276507260. S2CID  2484208.
13. Визель, Ю.; Вайсенбахер, Г.; Малик, С. (2015). «Решатели логической выполнимости и их применение при проверке моделей». Труды IEEE . 103 (11): 2021–2035. дои : 10.1109/JPROC.2015.2455034. S2CID  10190144.
14. Дуайер, М.; Аврунин Г.; Корбетт, Дж. (май 1999 г.). «Шаблоны в спецификациях свойств для проверки конечных состояний». Шаблоны в спецификации свойств для проверки конечных состояний. Материалы 21-й международной конференции по программной инженерии. стр. 411–420. дои : 10.1145/302405.302672. ISBN 1581130740.
15. * Проверка символической модели , Кеннет Л. Макмиллан, Kluwer, ISBN 0-7923-9380-5 , также онлайн. Архивировано 2 июня 2007 г. на Wayback Machine . 
16. «CUDD: Пакет схем решений CU» .
17. «BuDDy - Пакет схем двоичных решений» .
18. Кларк, Эдмунд; Грумберг, Орна; Джа, Сомеш; Лу, Юань; Вейт, Хельмут (2000), «Уточнение абстракции на основе контрпримеров», Компьютерная проверка (PDF) , Конспекты лекций по информатике, том. 1855, стр. 154–169, doi : 10.1007/10722167_15 , ISBN. 978-3-540-67770-3
19. Давар, А; Крейцер, С (2009). «Параметризованная сложность логики первого порядка» (PDF) . ЕССС . S2CID  5856640. Архивировано из оригинала (PDF) 03 марта 2019 г.
20. Проверка модели Storm
21. Зинг

дальнейшее чтение

• Пелед, Дорон А .; Пелличчоне, Патрицио; Сполетини, Паола (2009). «Проверка модели». Энциклопедия компьютерных наук и техники Wiley . стр. 1904–1920. дои : 10.1002/9780470050118.ecse247. ISBN 978-0-470-05011-8. S2CID  5371327.
• Кларк, Эдмунд М .; Грумберг, Орна ; Пелед, Дорон А. (1999). Проверка модели . МТИ Пресс . ISBN 0-262-03270-8.
• Берард, Б.; Бидуа, М.; Финкель, А.; Ларуссини, Ф.; Пети, А.; Петруччи, Л.; Шнобелен, П. Верификация систем и программного обеспечения: методы и инструменты проверки моделей . ISBN 3-540-41523-8.
• Хут, Майкл; Райан, Марк (2004). Логика в информатике: моделирование и рассуждения о системах . Издательство Кембриджского университета .
• Хольцманн, Джерард Дж. Проверка спиновой модели: учебник для начинающих и справочное руководство. Аддисон-Уэсли. ISBN 0-321-22862-6.
• Брэдфилд, Джулиан; Стирлинг, Колин (2001). «Модальная логика и мю-исчисление: Введение». Справочник по процессуальной алгебре . Эльзевир. стр. 293–330. дои : 10.1016/B978-044482830-9/50022-9. ISBN 978-0-444-82830-9.. Дж. А. Бергстра, А. Понсе и С. А. Смолка, редакторы». ().
• «Шаблоны спецификации». Лаборатория SAnToS, Университет штата Канзас. Архивировано из оригинала 19 июля 2011 г.
• «Сопоставления шаблонов свойств для RAFMC». CADP:Построение и анализ распределенных процессов . 2019.
• Матееску, Раду; Сигиряну, Михаэла (2003). «Эффективная проверка модели на лету для регулярного мю-исчисления без альтернатив» (PDF) . Наука компьютерного программирования . 46 (3): 255–281. дои : 10.1016/S0167-6423(02)00094-1. S2CID  10942856.
• Мюллер-Ольм, М.; Шмидт, Д.А.; Стеффен, Б. (1999). «Проверка модели: введение в учебное пособие». Статический анализ: 6-й международный симпозиум, SAS'99, Венеция, Италия, 22-24 сентября 1999 г., Труды . Том. 1694. LNCS: Спрингер. стр. 330–354. CiteSeerX  10.1.1.96.3011 . дои : 10.1007/3-540-48294-6_22. ISBN 978-3-540-48294-9.
• Байер, К. ; Катоен, Дж. (2008). Принципы проверки моделей . МТИ Пресс. ISBN 978-0-262-30403-0.
• Кларк, Э.М. (2008). «Рождение проверки моделей». 25 лет проверки моделей . Конспекты лекций по информатике. Том. 5000. стр. 1–26. дои : 10.1007/978-3-540-69850-0_1. ISBN 978-3-540-69849-4.
• Эмерсон, Э. Аллен (2008). «Начало проверки моделей: личный взгляд». В Грумберге, Орна; Вейт, Хельмут (ред.). 25 лет проверки моделей — история, достижения, перспективы. ЛНКС. Том. 5000. Спрингер. стр. 27–45. дои : 10.1007/978-3-540-69850-0_2. ISBN 978-3-540-69849-4.(это также очень хорошее введение и обзор проверки моделей)