■ ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 519.7
ПРИМЕНЕНИЕ МЕТОДА ФОРМАЛЬНЫХ УТВЕРЖДЕНИЙ О ТРАССАХ ДЛЯ СПЕЦИФИКАЦИИ, ПОСТРОЕНИЯ И ВЕРИФИКАЦИИ АВТОМАТНЫХ ПРОГРАММ*
© 2009 г. Е. В. Кузьмин, В. А. Соколов, Д. Ю. Чалый
Ярославский государственный университет им. П.Г. Демидова 150000 Ярославль, ул. Советская, 14 E-mail: kuzmin@uriiyar.ac.ru, sokolov@uriiyar.ac.ru, chaly@uniyar.ac.ru Поступила в редакцию 20.04.2008 г.
В статье рассматриваются перспективы использования метода формальных утверждений о трассах [1] как средства спецификации и верификации программ, построенных в автоматном стиле [2-4]. Метод формальных утверждений о трассах позволяет точно определить внешнее поведение автоматной программы, абстрагируясь от деталей ее реализации, и применяется на этапе определения технических требований (requirements specification) для создаваемой системы. В статье показано, как на основе созданной спецификации можно определять семантику некоторых элементов автоматной программы, прежде всего тех, которые используются при взаимодействии с объектом управления, а также описан формальный подход, помогающий задать множество состояний автоматной программы. Кроме рассмотрения способов построения автоматных программ, приведены результаты исследований, касающихся верификации требований, представленных в построенной спецификации.
1. ВВЕДЕНИЕ
В настоящее время многими исследователями отмечается (например, [5, 6]), что наиболее уязвимой и подверженной ошибкам частью создаваемых программно-аппаратных комплексов является именно программное обеспечение (ПО). Так, в [5] указывается, что причинами отсутствия доверия к ПО являются: история отказов ПО в прошлом (например, [7, 8]), трудности понимания и инспектирования ПО, сложность тестирования, отсутствие взаимного согласия между заказчиком и исполнителем о желаемых функциях ПО. Поэтому важной и актуальной задачей является разработка надежных методов проектирования, инспектирования, тестирования и верификации программных систем.
Несмотря на то, что к настоящему времени предложено множество подходов к разработке
* Работа поддержана грантом РФФИ №07-01-00702.
программного обеспечения (сравнительный анализ приведен в [9], обсуждение применительно к задачам логического управления можно найти в [2]), большинство из них сходится в том, что начальным этапом проектирования программной системы является определение технического задания (requirements specification) [6], или спецификации требований, которым должна удовлетворять построенная система (в дальнейшем мы будем использовать просто термин спецификация). Спецификация является главным источником информации о том, какие функции должна реализовывать система, однако спецификация не обязана накладывать каких-бы то ни было ограничений на то, каким образом система будет построена. На основе этого документа производится проектирование программной системы, создание программного кода, ее тестирование и верификация. Большинство исследователей сходится в том, что эффективный анализ, построение и верификация программных систем
возможно только с использованием точных математических методов на всех стадиях их разработки.
Именно в этом направлении развивается технология автоматного программирования [2-4], в рамках которой предлагаются новые формальные модели автоматных программ [10]. Эта технология предлагает способ построения программ в виде системы взаимодействующих конечных автоматов Мура-Мили. Проектирование каждого автомата состоит в создании по его словесному описанию схемы связей, описывающей его интерфейс, и графа переходов, определяющего его поведение. Однако использование неформальных описаний как отправной точки для построения системы взаимодействующих автоматов является слабым местом этой технологии, из-за которого возможны ошибки в автоматной программе. Действительно (см., например, [6, 11]), наиболее критичные ошибки в программных системах являются следствием недочетов, допущенных на стадии определения требований к системе, а их исправление на более поздних стадиях проектирования программы может быть на несколько порядков сложнее [12], чем своевременное устранение. Неформальная словесная постановка задачи значительно затрудняет корректное выделение всех существенных требований, предъявляемых заказчиком. Согласно [13], при чтении неформальной, словесной спецификации разработчик может столкнуться с неоднозначным толкованием, отсутствием ряда требований (неполнота спецификации), противоречивыми требованиями, отсутствием четкого изложения, а это все значительно затрудняет процесс анализа поставленной задачи и построения автоматной программы. Более того, возможно развитие ситуации, когда заказчик будет обнаруживать и устанавливать все новые требования к построенной программе и, следовательно, будет увеличиваться количество итераций "уточнение задачи"-"построение автоматной программы". Ситуация значительно усложняется, если разрабатывается автоматная программа для систем со "сложным поведением" [14], т.е. таких систем, поведение которых зависит не только от текущего состояния системы, но и от предыдущей истории работы. Поэтому необходимо средство, с помощью которого можно было бы проводить формальный анализ поставленной зада-
чи, постепенно ее уточняя и увеличивая степень понимания того, что должна делать программа. Этот метод должен быть достаточно абстрактным, чтобы можно было избежать фокусирования на внутренних, не видимых пользователю аспектах реализации. В качестве такого метода мы рассматриваем метод формальных утверждений о трассах (trace assertion method, ТАМ-метод) [1].
Статья построена следующим образом. Сначала описывается подход к спецификации автоматных программ - метод формальных утверждений о трассах (раздел 2). Далее, в разделе 3, рассматриваются основные концепции технологии автоматного программирования с использованием иерархической модели автоматных программ [10]. Применение спецификации для построения автоматных программ обсуждается в разделе 4. Далее, в разделе 5 мы обсуждаем вопросы верификации автоматных программ на основе построенной спецификации. Завершается статья выводами, которые включают возможные направления дальнейших исследований.
2. МЕТОД ФОРМАЛЬНЫХ УТВЕРЖДЕНИЙ О ТРАССАХ
Метод формальных утверждений о трассах был впервые предложен в статье Бартуссека и Парнаса [1]. Этот метод предназначен для спецификации программных модулей в соответствии с принципом сокрытия информации [15]. Таким образом, спецификации в терминах ТАМ-метода представляют собой описания в виде "черного ящика", т.е. видимыми являются только внешне наблюдаемые характерные черты модуля, а внутренние детали реализации скрыты. К настоящему времени были предложены несколько модификаций этого метода [16-18], существуют программные средства, поддерживающие его различные варианты [19, 20], а также этот метод был использован на практике для спецификации реальных управляющих систем [13, 21-23]. Таким образом, метод формальных утверждений о трассах представляет не только теоретический, но и практический интерес.
Для каждого модуля задается конечное число воздействий, которые могут изменить его поведение. В совокупности эти воздействия образу-
ют интерфейс модуля с внешней средой и могут представлять различные виды взаимодействия. В ответ на воздействия модуль может возвращать реакции во внешнюю среду. Метод формальных утверждений о трассах является способом описания внешне различимых режимов (или состояний) модуля с помощью конечных последовательностей событий, элементами которых являются пары "воздействие-реакция".
Пусть М - это некоторый программный модуль, для которого определено множество воздействий Рм = {pi, ■ ■ ■ ,Рп}, образующих его интерфейс с внешним миром. Пусть для каждого воздействия pi модуль может возвращать реакцию, являющуюся элементом из некоторого множества Гг-, и пусть Тм = Ui<i<nTi- Тогда трассой назовем последовательность р = pi1 :
оч.рг2 : ог2.ргз :огз.....pik : oik, где pim (1 m
^ к) обозначает воздействие, поданное на модуль, Oim G Tim обозначает возвращаемую реакцию, а с помощью "." обозначим операцию конкатенации. В том случае, если в ответ на некоторое воздействие не возвращается никакой реакции, считается, что возвращается реакция со специальным значением nil. Фактически трасса представляет собой цепочку, принадлежащую алфавиту А С Рм X Тм- Далее с помощью е мы будем обозначать пустую цепочку. Обозначения А* и Д+ будут задавать множества всех цепочек над алфавитом А с включением пустой цепочки в множество и без ее включения соответственно.
Обозначим через v: А* —> Тм U {nil} проекцию, которая задает значение последней реакции для произвольной трассы:
1. г/(е) = nil;
2. Ур : о G А 1у(р : о) = о;
3. Ух, у G Д+ v{x.y) = v(y)-
Обозначим через 7г: А* —> Р^ U {е} проекцию, которая для произвольной трассы определяет последовательность воздействий, оказываемых на модуль:
1. 7г(е) = е;
2. Ур : о £ А 7Г(р : о) = р;
3. Ух, у G А* 7т(х.у) = 7т(ж).7Г(у).
Назовем трассу s выполнимой, если для любых префиксов s' трассы s модуль допускает выполнение трассы s'. Выполнимые трассы определяют возможные сценарии использования модуля.
ЕСЛИ ДЛЯ Любых ВЫПОЛНИМЫХ ТраСС Si И S2 некоторого модуля М выполняется условие
Si = s2 7г(ж) = 7г(у),
то такой модуль называется независимым от реакций (output independent). Независимые от реакций модули не имеют "внутренней" памяти, в которой бы они хранили историю выходных реакций. Такие модули могут запоминать только историю поданных на вход воздействий. В статье рассматриваются только такие модули.
Назовем две выполнимые трассы si и s2 эквивалентными (и будем писать si = S2), если любое дальнейшее внешне обозримое поведение
модуля М после срабатывания любой из этих
Е
трасс является одним и тем же: si = тогда и только тогда, когда для любой трассы s G А* трассы s\.s и s2.s являются выполнимыми либо не выполнимыми одновременно. С помощью введенного отношения эквивалентности множество всех выполнимых трасс разбивается на классы эквивалентности. В нашей статье мы ограничимся р
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.