научная статья по теме МОДЕЛИРОВАНИЕ, СПЕЦИФИКАЦИЯ И ВЕРИФИКАЦИЯ "АВТОМАТНЫХ" ПРОГРАММ Математика

Текст научной статьи на тему «МОДЕЛИРОВАНИЕ, СПЕЦИФИКАЦИЯ И ВЕРИФИКАЦИЯ "АВТОМАТНЫХ" ПРОГРАММ»

ПРОГРАММИРОВАНИЕ, 2008, № 1, с. 38-60

ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ

УДК 519.687.1

МОДЕЛИРОВАНИЕ, СПЕЦИФИКАЦИЯ И ВЕРИФИКАЦИЯ

"АВТОМАТНЫХ" ПРОГРАММ

© 2008 г. Е. В. Кузьмин, В. А. Соколов

Ярославский государственный университет им. П.Г. Демидова 150000 Ярославль, ул. Советская, 14 E-mail: egorkuz@uriiyar.ac.ru, sokolov@uniyar.ac.ru Поступила в редакцию 04.10.2006 г.

1. ВВЕДЕНИЕ

Статья посвящена описанию, спецификации и верификации моделей программ, построенных на основе автоматного подхода к программированию [1-5].

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

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

"борьбу с ошибками" еще на стадии алгоритмизации.

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

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

Несмотря на то, что дедуктивный анализ [6] является очень трудоемким методом с сильной привязкой к семантике языка программирования и не может быть полностью автоматизирован и лишен контроля эксперта, он, тем не менее, при желании вполне может быть применим для "автоматных" программ после их полного построения непосредственно для проверки корректности процедур (написанных на некото-

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

С другой стороны, для проверки логики "автоматных" программ удобным является метод проверки модели [7]. При этом методе для программы строится формальная конечная модель (то есть с конечным числом состояний), а проверяемые свойства задаются с помощью формул темпоральной логики. Проверка выполнимости темпоральных формул, задающих свойства модели, происходит автоматическим образом. Важно отметить, что построение модели программы для автоматической верификации является весьма серьезной и сложной задачей. При построении модели для программы, написанной традиционным способом, возникает проблема адекватности этой программной модели исходной программе. Модель может не учитывать ряд программных свойств или порождать несуществующие свойства. Автоматный подход к программированию с точки зрения моделирования и анализа программных систем имеет ряд преимуществ по сравнению с традиционным подходом. При автоматном программировании не возникает проблемы адекватности модели, поскольку набор взаимодействующих автоматов, описывающий логику программы, уже является адекватной моделью, по которой формальным образом строится программный модуль. И это является бесспорным плюсом автоматной технологии. Более того, модель имеет конечное число состояний, что является необходимым на практике условием для успешной автоматической верификации, поскольку метод проверки на модели представляет собой переборный метод.

Одними из наиболее популярных темпоральных логик для спецификации и верификации свойств программных систем являются логика CTL (branching-time logic или computation tree logic) и логика линейного времени LTL (linear-

time logic). Для целей верификации автоматных программ логика LTL заслуживает особого внимания, поскольку любая формула в рамках этой логики по сути представляет собой автомат Бюхи, описывающий (принимающий) бесконечные допустимые пути структуры Крипке, которая, в свою очередь, задает поведение (все возможные исполнения) проверяемой на корректность "автоматной" модели. Это позволяет при спецификации и верификации "автоматных" программ оперировать в основном таким простым понятием, как "автомат".

Таким образом, перечисленное выше позволяет говорить о возможности эффективного применения для верификации "автоматных" программ (для анализа корректности логики "автоматных" программ) метода проверки модели.

Существует ряд программных средств верификации абстрактных моделей, построенных в рамках некоторых формализмов (сети Петри, взаимодействующие асинхронные процессы, автоматы с реальным временем, гибридные автоматы и т.д.), базирующихся на общих подходах и технологиях. Среди этих средств верификации классическим методом проверки модели можно выделить, например, CPNTools [8], SPIN [9], SMV [10] и CADP [11], использующие в качестве языков спецификации формальных моделей, соответственно, раскрашенные сети Петри высокого уровня, язык Promela, синхронные процессы и язык LOTOS. С одной стороны, можно считать, что целью создания такого рода программных продуктов является, главным образом, отработка тех или иных теоретических и прикладных методов верификации моделей, но в то же время многие из них имеют ориентированный на конкретную область применения язык спецификации - например, на моделирование и анализ коммуникационных протоколов или разработку синхронных аппаратных логических схем. Однако, программных средств верификации, направленных непосредственно на поддержку технологии автоматного программирования, не существует, что не исключает, а скорее предполагает активное использование уже имеющихся (проверенных временем) разработок ведущих лабораторий мира, которые обычно долгое время сопровождаются тематическими конференциями (зачастую полностью

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

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

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

2. ИЕРАРХИЧЕСКАЯ МОДЕЛЬ АВТОМАТНЫХ ПРОГРАММ ДЛЯ "РЕАКТИВНЫХ" СИСТЕМ И СИСТЕМ ЛОГИЧЕСКОГО УПРАВЛЕНИЯ

Рассмотрим иерархическую систему взаимодействующих детерминированных конечных автоматов

А = (Ао, Ац,..., ,..., АпI,..., Апк„))

где п ж ki (1 < I < п) - натуральные

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком