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

Область компьютерных наук

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

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

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

Обзор

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

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

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

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

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

Символическая проверка модели

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

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

Пример

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

${\displaystyle {\begin{aligned}\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{aligned}}}$

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

Методы

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

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

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

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

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

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

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

Инструменты

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

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

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

• Абстрактная интерпретация
• Автоматизированное доказательство теорем
• Диаграмма бинарных решений
• Büchi автомат
• Логика дерева вычислений
• Уточнение абстракции на основе контрпримера
• Формальная проверка
• Линейная временная логика
• Список инструментов проверки моделей
• Частичное уменьшение порядка
• Анализ программ (информатика)
• Статический анализ кода

Ссылки

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. Кларк, Э.М.; Эмерсон, Э.А.; Систла, А.П. (1986), «Автоматическая проверка конечных параллельных систем с использованием спецификаций темпоральной логики», ACM Transactions on Programming Languages ​​and Systems , 8 (2): 244, doi : 10.1145/5397.5399 , S2CID  52853200
7. Куэй, Дж. П.; Сифакис, Дж. (1982), «Спецификация и проверка параллельных систем в CESAR», Международный симпозиум по программированию , Lecture Notes in Computer Science, т. 137, стр. 337–351, doi :10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9
8. "Пресс-релиз: Премия ACM Turing Award вручается основателям технологии автоматической проверки". Архивировано из оригинала 28.12.2008 . Получено 06.01.2009 .
9. USACM: Объявлены победители премии Тьюринга 2007 года
10. Grobelna, Iwona; Grobelny, Michał; Adamski, Marian (2014). "Model Checking of UML Activity Diagrams in Logic Controllers Design". Труды Девятой международной конференции по надежности и сложным системам DepCoS-RELCOMEX. 30 июня – 4 июля 2014 г., Брунов, Польша . Advances in Intelligent Systems and Computing. Vol. 286. pp. 233–242. doi :10.1007/978-3-319-07013-1_22. ISBN 978-3-319-07012-4.
11. И. Гробельна, «Формальная проверка спецификации встроенного логического контроллера с помощью компьютерного вывода во временной логике», Przeglad Elektrotechniczny, том 87, выпуск 12a, стр. 47–50, 2011
12. Статья основана на материале, взятом из Model+checking в Free On-line Dictionary of Computing до 1 ноября 2008 года и включенном в соответствии с условиями «перелицензирования» GFDL версии 1.3 или более поздней.
13. Кларк, Э.; Бире, А.; Райми, Р.; Чжу, И. (2001). «Проверка ограниченной модели с использованием решения выполнимости». Формальные методы в проектировании систем . 19 : 7–34. doi :10.1023/A:1011276507260. S2CID  2484208.
14. Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). «Решатели булевой выполнимости и их применение в проверке моделей». Труды IEEE . 103 (11): 2021–2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
15. Дуайер, М.; Аврунин, Г.; Корбетт, Дж. (май 1999). «Шаблоны в спецификациях свойств для конечно-статусной верификации». Шаблоны в спецификации свойств для конечно-статусной верификации. Труды 21-й международной конференции по программной инженерии. стр. 411–420. doi :10.1145/302405.302672. ISBN 1581130740.
16. * Проверка символической модели , Кеннет Л. Макмиллан, Kluwer, ISBN 0-7923-9380-5 , также онлайн. Архивировано 2 июня 2007 г. на Wayback Machine . 
17. Coudert, O.; Madre, JC (1990). "Унифицированная структура для формальной проверки последовательных схем" (PDF) . 1990 IEEE Международная конференция по автоматизированному проектированию. Сборник технических документов . IEEE Comput. Soc. Press. стр. 126–129. doi :10.1109/ICCAD.1990.129859. ISBN 978-0-8186-2055-3.
18. «CUDD: Пакет схем решений CU» .
19. «BuDDy – Пакет диаграмм бинарных решений».
20. Кларк, Эдмунд; Грумберг, Орна; Джа, Сомеш; Лу, Юань; Вайт, Хельмут (2000), «Уточнение абстракции с помощью контрпримеров», Computer Aided Verification (PDF) , Lecture Notes in Computer Science, т. 1855, стр. 154–169, doi : 10.1007/10722167_15 , ISBN 978-3-540-67770-3
21. Давар, А; Крейцер, С (2009). «Параметризованная сложность логики первого порядка» (PDF) . ECCC . S2CID  5856640. Архивировано из оригинала (PDF) 2019-03-03.
22. Проверка модели шторма
23. Зинг

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

• Пелед, Дорон А .; Пелличчоне, Патрицио; Сполетини, Паола (2009). «Проверка модели». Энциклопедия компьютерных наук и техники Wiley . стр. 1904–1920. дои : 10.1002/9780470050118.ecse247. ISBN 978-0-470-05011-8. S2CID  5371327.
• Кларк, Эдмунд М.; Грумберг , Орна ; Пелед, Дорон А. (1999). Проверка моделей . MIT Press . ISBN 0-262-03270-8.
• Berard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P. (20 июня 2001 г.). Системы и проверка программного обеспечения: методы и инструменты проверки моделей . Springer. ISBN 3-540-41523-8.
• Хут, Майкл; Райан, Марк (2004). Логика в информатике: моделирование и рассуждения о системах . Cambridge University Press .
• Хольцманн, Джерард Дж. Проверка спиновых моделей: Учебное пособие и справочное руководство. Эддисон-Уэсли. ISBN 0-321-22862-6.
• Брэдфилд, Джулиан; Стирлинг, Колин (2001). «Модальные логики и мю-исчисления: Введение». Справочник по алгебре процессов . Elsevier. стр. 293–330. doi :10.1016/B978-044482830-9/50022-9. ISBN 978-0-444-82830-9.. Дж. А. Бергстра, А. Понсе и С. А. Смолка, редакторы». ().
• "Specification Patterns". Лаборатория SAnToS, Университет штата Канзас. Архивировано из оригинала 2011-07-19.
• «Отображения шаблонов свойств для RAFMC». CADP: Построение и анализ распределенных процессов . 2019.
• Матееску, Раду; Сигиряну, Михаэла (2003). «Эффективная проверка моделей на лету для регулярного мю-исчисления без чередования» (PDF) . Наука компьютерного программирования . 46 (3): 255–281. doi :10.1016/S0167-6423(02)00094-1. S2CID  10942856.
• Müller-Olm, M.; Schmidt, DA; Steffen, B. (1999). "Model verification: a tutorial introduction". Статический анализ: 6-й международный симпозиум, SAS'99, Венеция, Италия, 22-24 сентября 1999 г., Труды . Том 1694. LNCS: Springer. стр. 330–354. CiteSeerX  10.1.1.96.3011 . doi :10.1007/3-540-48294-6_22. ISBN 978-3-540-48294-9.
• Байер, К.; Катоен , Дж. (2008). Принципы проверки моделей . MIT Press. ISBN 978-0-262-30403-0.
• Кларк, Э. М. (2008). «Рождение проверки моделей». 25 лет проверки моделей . Конспект лекций по информатике. Том 5000. С. 1–26. doi :10.1007/978-3-540-69850-0_1. ISBN 978-3-540-69849-4.
• Эмерсон, Э. Аллен (2008). «Начало проверки моделей: личная точка зрения». В Грумберг, Орна; Вайт, Хельмут (ред.). 25 лет проверки моделей — история, достижения, перспективы. LNCS. Том 5000. Springer. стр. 27–45. doi :10.1007/978-3-540-69850-0_2. ISBN 978-3-540-69849-4.(это также очень хорошее введение и обзор проверки моделей)