АНАЛИЗ И ПРИМЕНЕНИЕ МЕТОДА ВЕРИФИКАЦИИ MODEL CHECKING

Введение в Model Checking

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

Model Checking – это метод позволяющий автоматически формально верифицировать системы, в том числе параллельные, с конечным числом состояний. Её цель – проверка того, удовлетворяет ли заданная модель системы заранее определённым требованиям. Таким образом, наш метод попадает под категорию формальных верификаций.

Формальная верификация, или как еще называют эти проверки, формальное доказательство — это метод формального доказательства соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства [1, с. 32]. Сама верификация несёт в себе формальное доказательство на основе абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ [2].

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

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

Рисунок 1. Процесс верификации

Реализация модели

В качестве модели обычно, используется так называемая модель Крипке [3], которая формально задаётся следующим образом:

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

Итак, Проверка модели позволяет разработчику обнаружить ошибку и исправить модель или требования. Если не найдено ни одной ошибки, разработчик может усовершенствовать описание модели (сделать модель более реалистичной, приняв во внимание больший набор свойств), как правило, увеличив ее размер, и перезапустить процесс верификации.

Рассмотрим достоинства и недостатки этого метода.

Достоинства:

• эффективность;
• возможность создания контрпримеров;

Недостатки:

• поддержка только конечных моделей;
• ограниченность верификации.

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

Список литературы:

1. Ю. Карпов. Model Checking. Верификация параллельных и распределенных программных систем 07.06.2010. URL: http://padabum.com/d.php?id=24324 (дата обращения: 02.11.19)
2. An introduction to model checking. URL: https://www.embedded.com/an-introduction-to-model-checking/ (дата обращения: 03.11.19)
3. S. Edelkamp. Automated System Verification // «Temporal logic» 03.02.2012. URL: https://www.sciencedirect.com/topics/computer-science/kripke-structure (дата обращения: 03.11.19)