shkolageo.ru 1


Model checking - метод верификации дискретных систем


Model checking – метод верификации, изменивший промышленность



Верификация



Model Checking –проверка на модели



Ограниченность классической логики для выражения свойств динамики (во времени)

  • Классическая логика высказываний (propositional logic)

    • Примитивная модель истины: “черно-белая” модель, высказывания статичны, неизменны во времени
  • Пример - некоммутативность конъюнкции, A&B  B&A:

    • “Джону стало страшно и он убил”  “Джон убил и ему стало страшно”
    • “Смит умер и его похоронили”  “Смита похоронили и он умер”
    • “Джейн вышла замуж и родила ребенка”  “Джейн родила ребенка и вышла замуж”
  • В обычной логике высказываний не формализуются:

    • Путин - президент России (истинно только в какой-то период)
    • Мы не друзья, пока ты не извинишься
    • Если m поступило на вход в канал, то потом m появится на выходе
    • Запрос к лифту c произвольного этажа, поступивший в любой момент времени, будет когда-нибудь в будущем удовлетворен


Tense Logic

  • Впервые - философ Diodorus Cronus



Дополнительные модальности TL: Until, X



LTL в дискретном времени – А. Пнуэли (1977)


Linear Temporal Logic (LTL)

  • Формальное определение темпоральной логики

    • Формула LTL это :
      • атомарное утверждение (атомарный предикат) p, q, ...,
      • или Формулы, связанные логическими операторами ,
      • или Формулы, связанные темпоральными операторами U, X
    • Прошлое обычно не рассматривают


Формализация высказываний в LTL

  • “Dum spiro, spero” - пока живу – надеюсь

    • G(я_живу  я_надеюсь)
  • “Мы придем к победе коммунистического труда!”

    • F коммунистический_труд_победил!
  • “Сегодня он играет джаз, а завтра Родину продаст!”

    • он_играет_джаз  Xон_продает_Родину – слишком буквально
    • G(он_играет_джаз  FXон_продает_Родину)
  • Раз Персил – всегда Персил

    • G(ПерсилGПерсил) – раз попробовав, будешь использовать всегда
  • Мы не друзья, пока ты не извинишься

    • Мы_друзья U Ты_извиняешься  G( Мы_друзья &Ты_извиняешься)


TL и анализ дискретных технических систем



Примеры формул LTL



Линейное и ветвящееся время



Логика ветвящегося времени – CTL*



LTL и CTL – подклассы CTL*



CTL – рекурсивное определение


Выражение свойств технических систем в логике ветвящегося времени CTL

  • EF(Start & Ready)

    • существует путь, на котором достижимо состояние, где Start выполняется, а Ready – нет
  • AG(Req AF Ack)

    • на любой полученный запрос Req всегда в будущем получим ответ Ack
  • AG[q  AX[A(p U r) AG r] ]

    • между q и r свойство р никогда не выполнится


Возможности спецификации и проверки требований

  • AGAF Restart

    • при любом функционировании системы (на любом пути) из любого состояния системы всегда обязательно вернемся в состояние рестарта
  • EF( int >0.01)

    • не существует такого режима работы прибора, при котором интенсивность облучения пациента превысит 0.01 радиан в сек
  • AG(antiFire_is_on  P captain_Permission)

    • в любом режиме, если противопожарная система включается, то на это обязательно предварительно была получена санкция капитана
  • AG (req3  (req3 U ack))

    • во всех режимах после того, как запрос req3 установится, он никогда не будет снят, пока на него не придет подтверждение
  • E[ p U A [q U r] ]

    • cуществует режим, в котором условие p будет истинным с начала вычисления до тех пор, пока q не станет непрерывно активно до выполнения r


Пример свойства логики CTL

  • Любой грешник всегда имеет шанс вернуться на путь истинной веры:



Общая схема верификации для СTL



Model Checking для CTL – проверка на развертке (неформально)



Model checking для CTL



Алгоритм разметки состояний для CTL



Model checking для одного из базисов CTL



Model Checking – пример анализа


Model Checking для LTL

  • Строить алгоритм проверки модели для LTL-формулы, перебирая все пути – бессмысленно

  • Другой метод – проверить, есть ли контрпримеры, т.е. проверить, есть ли вычисления, удовлетворяющие Ф. Единственный контрпример достаточен, чтобы опровергнуть К |= АФ

  • Для этого опишем конечным образом все вычисления, НЕ удовлетворяющие Ф

  • Проверим, есть ли пересечения с вычислениями К


Контрольный автомат - один из методов



Как найти пересечение языков: КА



Как найти пересечение языков: КА

  • Синхронная композиция автоматов – это просто два автомата, стоящих рядом

  • Язык, допускаемый автоматом A B – это пересечение языков, допускаемых каждым автоматом, и А, и В



Model Checking для LTL: автоматы Бюхи



Примеры автоматов Бюхи, допускающих цепочки, удовлетворяющие LTL формулам



Примеры автоматов Бюхи, допускающих цепочки, удовлетворяющие LTL формулам



Model Checking для LTL

  • Общий алгоритм проверки выполнимости формулы LTL для структуры Крипке К:

  • 1. По структуре К строится автомат Бюхи АК. Этот автомат допускает все возможные вычисления структуры К

  • 2. По формуле LTL Ф строится автомат Бюхи ВФ, допускающий множество вычислений, которые удовлетворяют Ф

  • 3. Строится автомат АК ВФ. Этот автомат – синхронная композиция автоматов АК и ВФ, допускает пересечение языков, допускаемых каждым компонентным автоматом

  • 4. Формула Ф выполняется для К, если и только если АК ВФ допускает пустой язык



Model Checking для LTL: Пример



Система верификации Spin



Пример: отчет фирмы Rockwell Collins 2007г.

















Cambridge ring protocol

    • Cambridge ring protocol
    • IЕЕЕ Logical Link Control protocol, LLC 802.2
    • фрагменты больших протоколов XTP и TCP/IP
    • отказоустойчивые системы, протоколы доступа к шинам, протоколы контроля ошибок в аппаратуре,
    • криптографические протоколы
    • протокол Ethernet Сollision Avoidance
    • DeepSpace1 (NASA). Уже после тщательного тестирования и сдачи системы были найдены несколько критических ошибок




Success Story. Транзакционная память в многоядерных процессорах

  • Транзакционная память – один из очень удобных способов, позволяющих избежать проблем синхронизации процессов над общей памятью



“Оконный” алгоритм транзакционной памяти

  • Michel Raynal в 2009 г. предложил один из алгоритмов транзакционной памяти

  • Michel Raynal has been a professor of computer science since 1981. At IRISA (CNRS-INRIA-University joint computing research laboratory located in Rennes), he founded a research group on Distributed Algorithms in 1983.


Success Story. Ошибка в STM протоколе

  • Imbs D.; Raynal M. Software Transactional Memories: an Approach for Multicore Programming. In 10th International Conference on Parallel Computing Technologies (PaCT'09), Aug., 2009/ LNCS – Работа, представляющая новый протокол транзакционной памяти и его (ручное) доказательство

  • Работа была дана Алексею Беляеву (в то время студенту 4 курса) для проверки протокола в рамках его НИРС

  • При верификации студент нашел ошибку в протоколе, разработанном и доказанном крупнейшими специалистами в этой области


Лучший доклад на конференции на ФизТехе в Москве



Литература

  • E. M.Clarke, O. Grumberg, D.Peled. Model checking. 1999

    • (Pусский перевод: Э.М.Кларк, О.Грамберг, Д.Пелед. Верификация моделей программ: Model Checking. М.,2002)
  • B.Berard et.al. Systems and Software Verification. Model checking Techniques and Tools // Springer, 1999

  • M.Huth, M.Ryan. Logic in Computer Science: Modelling and Reasoning about Systems Cambridge U // 1999

  • C.Baier, J.P.Katoen. Principles of Model checking // 2008

  • M. Ben-Ari. Principles of Spin Model Checker // 2008

  • Ю.Г.Карпов. Model checking. Верификация параллельных и распределенных программных систем // БХВ. Петербург, 2010

  • Множество статей, выложенных в Интернет курсов



Заключение

  • Model checking – достигшая зрелости область формального анализа, интенсивно использующаяся для верификации дискретных систем

  • Model checking имеет множество применений в разнообразных областях анализа динамических систем

  • Существует ряд проблем, препятствующих простому применению этого подхода в индустрии разработки ПО

  • В настоящее время - это область интенсивных исследований