Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Эта статья о проверке моделей в информатике. Для проверки моделей в статистике см. Проверка статистической модели .
Лифт Управляющее программное обеспечение может быть модель проверена , чтобы проверить оба свойства безопасности, как «The каюту никогда не движется с ее открытой дверью» , [1] и живучести свойства, как «Всякий раз , когда п - го Floor по вызова кнопка нажата, то кабина будет в конечном счете , остановка на n- м этаже и откройте дверь » .

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

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

Обзор [ править ]

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

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

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

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

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

Проверка символьной модели [ править ]

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

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

Пример [ править ]

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

Здесь следует читать как «всегда», как «в конце концов», как «до», а другие символы являются стандартными логическими символами для «или», для «и» и для «не».

Методы [ править ]

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

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

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

Логика первого порядка [ править ]

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

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

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

Инструменты [ править ]

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

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

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

См. Также [ править ]

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

Ссылки [ править ]

Цитаты [ править ]

  1. ^ Для удобства здесь примеры свойств перефразированы на естественном языке. Для проверки моделей требуется, чтобы они были выражены в некоторой формальной логике, например LTL .
  2. ^ Лам К., Уильям (2005). «Глава 1.1: Что такое проверка дизайна?» . Проверка конструкции оборудования: моделирование и подходы на основе формальных методов . Проверено 12 декабря 2012 года .
  3. ^ "Амир Пнуэли - лауреат премии AM Тьюринга" .
  4. ^ Аллен Эмерсон, E .; Кларк, Эдмунд М. (1980), "Характеризуя корректности свойств параллельных программ с использованием твердых точек", автоматные, Языки и программирование , Lecture Notes в области компьютерных наук, 85 : 169-181, DOI : 10.1007 / 3-540-10003-2_69 , ISBN 978-3-540-10003-4
  5. ^ Эдмунд М. Кларк, Э. Аллен Эмерсон: «Дизайн и синтез скелетов синхронизации с использованием временной логики ветвления времени» . Логика программ 1981: 52-71.
  6. ^ Кларк, EM; Эмерсон, EA; Sistla, AP (1986), "Автоматическая проверка конечно-параллельных систем с использованием временной логики спецификации", ACM Сделки по Языки программирования и системы , 8 (2): 244, DOI : 10,1145 / 5397.5399
  7. ^ Queille, JP; Сифакис, Дж. (1982), «Спецификация и проверка параллельных систем в CESAR», Международный симпозиум по программированию , конспект лекций по информатике, 137 : 337–351, DOI : 10.1007 / 3-540-11494-7_22 , ISBN 978-3-540-11494-9
  8. ^ "Пресс-релиз: Премия ACM Turing награждает основателей технологии автоматической проверки" . Архивировано из оригинала на 2008-12-28 . Проверено 6 января 2009 .
  9. ^ USACM : 2007 Тьюринга Объявлены победители
  10. ^ Гробельна, Ивона; Гробельный, Михал; Адамски, Мариан (2014). «Проверка моделей диаграмм активности UML при проектировании логических контроллеров». Материалы Девятой Международной конференции по надежности и сложным системам DepCoS-RELCOMEX. 30 июня - 4 июля 2014 г., Брунув, Польша . Достижения в интеллектуальных системах и вычислениях. 286 . С. 233–242. DOI : 10.1007 / 978-3-319-07013-1_22 . ISBN 978-3-319-07012-4.
  11. ^ I. Grobelna, " Формальная проверка спецификации встроенного логического контроллера с компьютерным выводом в темпоральной логике ", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47-50, 2011
  12. ^ Кларк, E .; Biere, A .; Raimi, R .; Чжу, Ю. (2001). «Ограниченная проверка модели с использованием решения по выполнимости». Формальные методы в системном дизайне . 19 : 7–34. DOI : 10,1023 / A: 1011276507260 .
  13. ^ Vizel, Y .; Weissenbacher, G .; Малик, С. (2015). "Решатели логической выполнимости и их приложения в проверке моделей". Труды IEEE . 103 (11): 2021–2035. DOI : 10.1109 / JPROC.2015.2455034 .
  14. ^ Дуайер, М .; Авруин, Г .; Корбетт, Дж. (Март 1998 г.). Ардис, М. (ред.). Шаблоны в спецификации свойств для проверки конечного состояния (PDF) . Труды Второго семинара по формальным методам в практике программного обеспечения. С. 7–15.
  15. ^ * Проверка символической модели , Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5 , также онлайн. Архивировано 2 июня2007 г. на Wayback Machine . 
  16. ^ "CUDD: Пакет схемы решений CU" .
  17. ^ «BuDDy - Пакет двоичных диаграмм решений» .
  18. ^ Кларк, Эдмунд; Грумберг, Орна; Джа, Сомеш; Лу, Юань; Вейт, Helmut (2000), "контрпример-Guided Абстракция Доработка" (PDF) , Computer Aided Проверка , Lecture Notes в области компьютерных наук, 1855 : 154-169, DOI : 10.1007 / 10722167_15 , ISBN  978-3-540-67770-3
  19. ^ Давар, А; Крейцер, С (2009). «Параметризованная сложность логики первого порядка» (PDF) . ECCC .
  20. ^ Зинг

Источники [ править ]

  • Эта статья основана на материалах, взятых из Free On-line Dictionary of Computing до 1 ноября 2008 г. и включенных в соответствии с условиями «перелицензирования» GFDL версии 1.3 или новее.

Дальнейшее чтение [ править ]

  • Проверка моделей , Дорон А. Пелед , Патрицио Пелличчионе, Паола Сполетини, Энциклопедия компьютерных наук и инженерии Wiley, 2009.
  • Проверка модели , Эдмунд М. Кларк , Орна Грумберг и Дорон А. Пелед, MIT Press , 1999, ISBN 0-262-03270-8 . 
  • Проверка систем и программного обеспечения: методы и инструменты проверки моделей , Б. Берард, М. Бидойт, А. Финкель, Ф. Ларуссини, А. Пети, Л. Петруччи, П. Шнебелен, ISBN 3-540-41523-8 
  • Логика в компьютерных науках: моделирование и рассуждения о системах , Майкл Хут и Марк Райан, Cambridge University Press , 2004. doi : 10.2277 / 052154310X .
  • Средство проверки спиновой модели: учебник и справочное руководство , Джерард Дж. Хольцманн , Аддисон-Уэсли, ISBN 0-321-22862-6 . 
  • Джулиан Брэдфилд и Колин Стирлинг, Модальные логики и мю-исчисления, Inf.ed.ac.uk
  • Спецификация Выкройки KSU.edu
  • Сопоставление шаблонов свойств для RAFMC Inria.fr
  • Раду Матееску и Михаэла Сигиреану Эффективная проверка модели на лету для регулярного Mu-исчисления без чередования , стр. 6, Наука компьютерного программирования 46 (3): 255–281, 2003
  • Мюллер-Ольм, М., Шмидт, Д.А. и Штеффен, Б. Проверка моделей: введение в учебное пособие. Proc. Шестой симпозиум по статическому анализу, Г. Файл и А. Кортези, редакторы, Springer LNCS 1694, 1999, стр. 330–354.
  • Байер, К. , Катоен, Дж .: Принципы проверки модели. 2008 г.
  • Э.М. Кларк : «Рождение модели проверки» doi : 10.1007 / 978-3-540-69850-0_1
  • Э. Аллен Эмерсон (2008). «Начало проверки модели: личная перспектива». В Орне Грумберг; Гельмут Вейт (ред.). 25 лет проверки моделей - история, достижения, перспективы . LNCS. 5000 . Гейдельберг: Springer. С. 27–45. ISBN 978-3-540-69849-4. (это также очень хорошее введение и обзор проверки модели)