Телефон: +7 (383)-202-16-86

Статья опубликована в рамках: Научного журнала «Студенческий» № 36(80)

Рубрика журнала: Информационные технологии

Библиографическое описание:
Останин М.Л. АНАЛИЗ И ПРИМЕНЕНИЕ МЕТОДА ВЕРИФИКАЦИИ MODEL CHECKING // Студенческий: электрон. научн. журн. 2019. № 36(80). URL: https://sibac.info/journal/student/80/156535 (дата обращения: 16.11.2019).

АНАЛИЗ И ПРИМЕНЕНИЕ МЕТОДА ВЕРИФИКАЦИИ 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)

Оставить комментарий