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

Эта статья о проверке моделей в информатике. Для проверки моделей в статистике см. Проверка статистической модели .

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

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

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

Обзор

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

Важный класс методов проверки моделей был разработан для проверки моделей аппаратных и программных средств , спецификация которых задается формулой временной логики . Новаторскую работу в области спецификации темпоральной логики провел Амир Пнуэли , получивший в 1996 году премию Тьюринга за «новаторскую работу по внедрению темпоральной логики в информатику». Проверка моделей началась с новаторских работ Э.М. Кларка , Э.А. Эмерсона , Дж. П. Кейль и Дж. Сифакис . Кларк, Эмерсон и Сифакис получили премию Тьюринга 2007 года за плодотворную работу по созданию и развитию области проверки моделей.

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

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

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

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

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

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

Пример

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

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

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

Техники

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

1. Символьные алгоритмы избегают явного построения графа для конечных автоматов (FSM); вместо этого они представляют график неявно, используя формулу количественной логики высказываний. Использование бинарных диаграмм решений (BDD) стало популярным благодаря работе Кена Макмиллана. а также Оливье Кудерта и Жана-Кристофа Мадра, и разработка библиотек манипуляции BDD с открытым исходным кодом, таких как CUDD. и БаДДи.
2. Ограниченные алгоритмы проверки модели разворачивают автомат за фиксированное количество шагов. $k$и проверьте, может ли произойти нарушение собственности в $k$ или меньше шагов. Обычно это предполагает кодирование ограниченной модели как экземпляра SAT . Процесс можно повторять с все большими и большими значениями $k$ до тех пор, пока все возможные нарушения не будут исключены (см. Итеративный поиск в глубину с углублением ).
3. Абстракция пытается доказать свойства системы, сначала упрощая ее. Упрощенная система обычно не обладает теми же свойствами, что и исходная, поэтому может потребоваться процесс ее усовершенствования. Как правило, требуется, чтобы абстракция была обоснованной (свойства, доказанные в абстракции, верны для исходной системы); однако иногда абстракция не является полной (не все истинные свойства исходной системы верны и для абстракции). Примером абстракции является игнорирование значений небулевых переменных и рассмотрение только логических переменных и потока управления программой; такая абстракция, хотя она и может показаться грубой, на самом деле может быть достаточной, чтобы доказать, например, свойства взаимного исключения .
4. Уточнение абстракции на основе контрпримеров (CEGAR) начинает проверку с грубой (то есть неточной) абстракции и итеративно уточняет ее. Когда обнаруживается нарушение (т. е. контрпример ), инструмент анализирует его на предмет осуществимости (т. е. является ли нарушение подлинным или является результатом неполной абстракции?). Если нарушение допустимо, об этом сообщается пользователю. Если это не так, доказательство невыполнимости используется для уточнения абстракции и проверка начинается заново.

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

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

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

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

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

Инструменты

Основная статья: Список инструментов проверки моделей

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

• 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 : общий инструмент для проверки правильности моделей распределенного программного обеспечения строгим и в основном автоматизированным способом.
• Шторм : Средство проверки моделей для вероятностных систем.
• TAPA : инструмент для анализа алгебры процессов
• TAPAAL : интегрированная инструментальная среда для моделирования, проверки и верификации сетей Петри с временной дугой.
• TLA+ Средство проверки модели от Лесли Лэмпорта
• UPPAAL : интегрированная инструментальная среда для моделирования, проверки и верификации систем реального времени, смоделированных как сети синхронизированных автоматов.
• Зинг – экспериментальный инструмент от Microsoft для проверки моделей состояния программного обеспечения на различных уровнях: высокоуровневые описания протоколов, спецификации рабочих процессов, веб-сервисы, драйверы устройств и протоколы ядра операционной системы. В настоящее время Zing используется для разработки драйверов для Windows.

См. также

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

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

• Пелед, Дорон А .; Пелличчоне, Патрицио; Сполетини, Паола (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 . (это также очень хорошее введение и обзор проверки моделей)