автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Теория конформности для функционального тестирования программных систем на основе формальных моделей

Институт Системного Программирования Российской Академии Наук

На правах рукописи

БУРДОНОВ Игорь Борисович

Теория конформности для функционального тестирования программных систем на основе формальных моделей

специальность 05.13 11 -математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени доктора физико-математических наук

П11Н1Ш1111

□□3166612

Москва - 2007

Работа выполнена в Институте Системного Программирования РАН

Официальные оппоненты: доктор технических наук,

профессор

Евтушенко Нина Владимировна

доктор физико-математических наук, профессор,

Крюков Виктор Алексеевич

доктор физико-математических наук, профессор

Подловченко Римма Ивановна

Ведущая организация: факультет Вычислительной Математики и

Кибернетики МГУ им. М В Ломоносова

Защита диссертации состоится «28» марта 2008 г в_часов на заседании

диссертационного совета Д.002 087 01 при Институте Системного Программирования РАН по адресу:

109004, Москва, Б Коммунистическая 25, Институт Системного Программирования РАН, конференц-зал

С диссертацией можно ознакомиться в читальном зале библиотеки Института Системного Программирования РАН

Автореферат диссертации разослан «_»_2008 г

Ученый секретарь диссертационного совета кандидат физико-математических наук

/С П Прохоров/

Актуальность исследования

От создания программ к тестированию программ

История информационных технологий - это, прежде всего, история их проникновения во все сферы деятельности человека, экономику, военную область, науку, образование, культуру и т.д Они становятся все более неотъемлемой частью инфраструктуры современной жизни Этот процесс, естественно, вызывает интенсивное развитие самих этих технологий создаются всё более мощные компьютеры и компьютерные системы, всё более сложные программы и программные комплексы

Однако, чем шире распространяется использование компьютеров, чем более важные и ответственные задачи возлагаются на их «плечи», тем выше становится цена ошибок в программно-аппаратных средствах Только в США потери от этих ошибок составляют от 20 до 60 млрд долларов ежегодно, причем около 60% убытков терпят конечные пользователи Складывается ситуация, когда производители выпускают, а потребители вынуждены оплачивать заведомо бракованный товар Но дело не только в материальном ущербе некорректное поведение компьютерных систем способно вызвать дезорганизацию управления государством, привести к техногенным и экологическим катастрофам, поставить под угрозу жизнь и здоровье людей

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

Ключевой частью решения этой проблемы является тестирование программ, часто требующее времени и ресурсов больше, чем создание этих программ Из второстепенной и как бы «побочной» деятельности тестирование

выходит на первый план, интегрируется с самим процессом разработки ПО и существенно изменяет представления о том, как надо создавать сложные программные комплексы Тестирование становится жесткой «обратной связью», замыкает «жизненный цикл» разработки ПО и перестраивает пространственно-временную структуру процесса разработки и организацию коллектива разработчиков

Тестирование на основе формальных моделей

В то же время высокая трудоемкость (для многих неожиданная) этой второй части процесса разработки ПО - тестирования, вынудила заняться поисками технологий, позволяющих сделать это более эффективно Разрабатываются как техники, обеспечивающие корректность ПО «по построению», так и более эффективные методы проверки правильности уже созданных программ

Последние десятилетия на стыке теории и практики информационных технологий складывается новая дисциплина — тестирование на основе моделей Это актуальное направление во многом опирается на работы различных исследователей, выполненные в 80-х и в 90-х годах прошлого века и посвященные проблемам тестирования телекоммуникационных протоколов Самые первые же статьи, которые с полным правом можно отнести к этой области, появились еще в конце 60-х — начале 70-х годов Тем не менее, серьезный практический и массовый интерес к ее результатам возник только на рубеже веков, в связи с востребованностью эффективных методов контроля и обеспечения качества сложных программных и программно-аппаратных систем в индустрии Тестирование на основе моделей начинает применяться в промышленных компаниях Первые же успехи (и, в не меньшей степени, первые неудачи) сделали разработку формальных методов тестирования чрезвычайно актуальными на сегодняшний день.

Основная идея тестирования на основе моделей вполне прозрачна поскольку сложная система не поддается проверке «в лоб», создайте сначала более простую ее модель, описав в ней только то, что для вас важно на

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

Модели должны быть одновременно достаточно просты, чтобы поддаваться строгому анализу, и достаточно универсальны, чтобы описывать большой класс практически важных систем. Возможность строгого анализа свойств модели становится актуальной, если необходимы определенные гарантии того, что все важные аспекты поведения системы покрываются построенными тестами Такие модели должны быть формальны, то есть описаны на языке математики Само же тестирование строится на некоторой математической теории, предписывающей определенные способы построения тестов, которые обеспечат им нужные свойства полноты, а тестированию придадут необходимую глубину и надежность

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

что реализационная модель неизвестна или слишком сложна для анализа Поэтому основной задачей является генерация по заданной спецификации модельных тестов, назначение которых - проверить конформность любой реализационной модели Эта проверка основана на модели взаимодействия реальной системы с ее окружением После того, как такие тесты созданы, они транслируются в реальные тестовые программы, которые, взаимодействуя с реальной системой, устанавливают ее соответствие или несоответствие исходным требованиям Эта схема работы основана на предположении, что не только моделирование требований в виде спецификации и трансляция модельных тестов в реальные программы выполнены правильно, но также соответствие требованиям правильно отражено в отношении конформности, а реальное взаимодействие отражено в модельном взаимодействии реализационных моделей и модельных тестов

Спецификация неоднозначно определяет реализацию, оставляя разработчику значительную свободу в рамках специфицированных требований Как именно нужно понимать эти требования, в чем разработчик свободен, а в чем «скован» требованиями, как раз и описывается отношением конформности Оно определяется предполагаемыми правилами взаимодействия системы с окружением, которые должны быть адекватно отражены на уровне моделей Спецификация не требует от реализации правильного поведения при взаимодействии с любым ее окружением, а только с таким, которое само ведет себя правильно Например, в терминах пред- и постусловий тесты должны проверять выполнение постусловия (программа работает правильно) только при таком взаимодействии, которое не нарушает предусловий (к программе правильно обратились) При тестировании правила взаимодействия как раз и определяют те тестовые возможности по управлению и наблюдению за тестируемой системой, которые необходимы и достаточны для проверки конформности

К созданию общей теории конформности

По поводу вида моделей, которые нужно использовать для описания сложных систем, большинство исследователей сейчас еще не пришли к общему мнению Чаще всего используются модели в виде различных разновидностей конечных автоматов (finite automata, finite state machines, FSM) и обобщающих их систем помеченных переходов (labeled transition systems, LTS) В диссертационной работе рассматривается последний вид моделей

Что же касается используемого при построении тестов отношения конформности, то на этот счет имеются десятки различных точек зрения В 1990-93 г г Ван Глаббек сумел классифицировать для LTS многие из этих отношений, описав 155 семантик взаимодействия, на которых такие конформности основаны. Однако даже он не учитывал многие семантики, специфические для реактивных систем В таких системах взаимодействие заключается в обмене порциями информации или «сообщениями» Специфичность проявляется в том, что семантика «сообщений» зависит от направления передачи из внешнего мира в систему (стимулы) или из системы во внешний мир (реакции) В частности, конечные автоматы являются такими реактивными системами, в которых на каждый посылаемый стимул в ответ выдается ровно одна реакция.

Для многих отношений конформности в последние годы были созданы соответствующие математические теории, на основе которых разработаны методы генерации тестов и построены практически используемые тестовые инструменты При этом каждый автор, предлагавший своё отношение конформности, формально начинал теорию «с нуля», и больше внимания уделял тому, чтобы показать превосходство своей конформности над другими, чем поиску общих идей и методов В результате имеется настолько большое разнообразие предлагаемых формализмов, методов и инструментов тестирования, что тестировщик оказывается перед серьезной проблемой выбора того, что ему подходит Вместе с тем сегодня уже становится ясно, что такие общие идеи и методы «витают в воздухе», поскольку в математических

формализмах различных конформностей и методах генерации тестов по этим конформностям очень много общего

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

Семантика наблюдаемого поведения

Среди отношений конформности выделяется большой класс отношений, основанных только на наблюдаемом поведении системы и не учитывающих ее внутреннего устройства В моделях внутреннее устройство системы отражается, прежде всего, в понятии состояния, которое является абстракцией таких объектов как переменные программы или поля данных объектов классов Сложность проверки таких конформностей связана с тем, что состояние, не наблюдаемое извне, тем не менее, влияет на дальнейшее наблюдаемое поведение реализации Тестирование на основе таких конформностей иногда называют тестированием «черного ящика» тест может только извне взаимодействовать с системой, но не знает и не видит ее внутреннего устройства. Такое тестирование называют также функциональным, акцентируя внимание на том, что оно проверяет только те свойства системы, которые отражаются в ее функциональности и наблюдаемы при ее функционировании Понятно, что такое тестирование имеет важное практическое значение, поскольку в реальных случаях состояния реализации часто недоступны тесту (например, при удалённом взаимодействии) Но более важно то, что учет состояний может оказаться «переспецификацией», поскольку требует от реализации того, что никак не проявляется при взаимодействии с ней

При тестировании методом «чёрного ящика» мы можем наблюдать только такое поведение реализации, которое, во-первых, «спровоцировано» тестом (управление) и, во-вторых, наблюдаемо во внешнем взаимодействии Такое

взаимодействие может моделироваться с помощью, так называемой, машины тестирования (Милнер и Ван Глаббек) Управление сводится к тому, что оператор машины, выполняя тест, нажимает какие-то кнопки, «приказывая» или «разрешая» реализации выполнять те или иные действия, которые могут им наблюдаться Наблюдения (на «дисплее» машины) бывают двух типов наблюдение некоторого действия, разрешённого оператором и выполняемого реализацией, и наблюдение отказа как отсутствия каких бы то ни было действий из числа тех, что разрешены нажатыми кнопками

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

В то же время разрешаемое множество действий - это, вообще говоря, не любое подмножество множества всех действий В вопросе о том, какие множества действий могут разрешаться тестом, а какие нет, среди исследователей существует большое разнообразие точек зрения Например, для реактивных систем обычно считается, что нельзя (или бессмысленно) смешивать посылку стимулов с приемом реакций (Ян Тритманс) Но существует и прямо противоположный подход нельзя «тормозить» выдачу реакций реализацией, поэтому, даже посылая стимул, тест должен быть готов к приему любой реакции (А Ф Петренко)

Также следует подчеркнуть, что наблюдение отказа возможно не при любом множестве разрешенных действий И здесь разные исследователи опираются на разные предположения Для тех же реактивных систем долгое

время считалось, что тест может наблюдать отсутствие реакций (quiescence, стационарность), например, по тайм-ауту, но не видит, принимает реализация посланный ей стимул или нет (input refusal, блокировка стимула) С другой стороны, в последние годы появляется все больше и больше работ, в которых такие блокировки стимулов допускаются или допускаются частично Также и реакции, если они принимаются тестом по разным «выходным каналам», можно принимать не все, а лишь те, что относятся к одному или нескольким выбранным каналам, что дает наблюдение частичной стационарности

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

К этому классу относятся такие семантики и отношения конформности как трассовая семантика {trace semantics) и трассовый предпорядок (tr - trace preorder), семантика завершенных трасс {completed trace semantics) и предпорядок завершенных трасс {ct - completed trace preorder), семантика трасс с отказами (failure trace semantics или refusal semantics) и предпорядок трасс с отказами (failure trace preorder или rf - refusal preorder), семантика для реактивных систем без блокировки стимулов, но с возможностью наблюдения отсутствия реакций, и отношения ior {input-output refusal relation или repetitive quiescence relation) и ioco (input-output conformance), семантика для реактивных систем с блокировками стимулов и отношение ioco^, (модификация отношения ioco, учитывающая блокировку стимулов), семантика для систем с мультиканалами стимулов и реакций (MOTS - Multi Input-Output Transition Systems) и отношение mioco (модификация отношения ioco для таких систем) и др За рамками этого класса оказываются различные симуляции — отношения конформности, основанные на соответствии состояний реализации и спецификации.

и

Задача создания теории конформности для класса семантик, основанных только на наблюдаемом поведении, является важнейшей и наиболее актуальной частью проблемы общей теории конформности

Семантика ненаблюдаемого поведения

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

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

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

дивергенцию на всех уровнях, мы выбрасываем из рассмотрения целый класс работоспособных систем

Что касается запрещенного (не декларированного) поведения, то этой теме посвящено очень мало работ Лишь в редких случаях вводятся запрещенные состояния, в которые реализация не должна попадать Между тем, поведение реализации должно быть полностью декларировано не всегда, а лишь при некоторых взаимодействиях окружения с ней Примером может служить поведение программы в зависимости от выполнения или нарушения предусловия обращения к ней в первом случае поведение реализации декларировано постусловием, а во втором случае полностью неопределенное Это означает, что спецификация должна не только описывать требуемое поведение реализации, но и отмечать те места, где поведение запрещено (не декларировано) В частности, эта тема весьма актуальна в теории и практике информационной безопасности, где система считается безопасной, если в ней нет недекларированного поведения В то же время, такая система может быть построена из компонентов, которые сами по себе не являются безопасными, но недекларированное поведение недостижимо при работе системы в целом за счет того, что каждый компонент взаимодействует не с произвольным окружением, а с заданными компонентами системы

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

Проблема композиции

Последние годы большое внимание уделяется тестированию составных систем, которые компонуются инкрементально и иерархически из компонентов

разных уровней Основная проблема композиции - это проблема соотношения спецификации системы и спецификаций ее компонентов Это соотношение корректно, если композиция компонентов, конформных своим спецификациям, всегда конформна спецификации системы. К сожалению, это не всегда так Проверку правильности такого соотношения иногда называют верификацией декомпозиции системных требований

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

Отсутствие решения проблемы монотонности препятствует верификации системных требований Наоборот, если найти такое решение, то можно не только верифицировать на корректность имеющуюся спецификацию системы, но и автоматически получить такую корректную спецификацию по заданным спецификациям компонентов Сгенерированная спецификация системы может использоваться как описание системы для ее пользователей, как «техническое задание» разработчику системы при дальнейших модификациях системы и ее компонентов, когда предполагается сохранение внешней функциональности системы (регрессионное тестирование), и, наконец, для генерации системных тестов

Частным случаем проблемы композиции является асинхронное тестирование или тестирование в контексте Такое тестирование можно рассматривать как тестирование системы из двух компонентов, один из которых - реализация, а другой - фиксированная среда передачи Этот частный случай очень важен, поскольку практическое тестирование почти всегда

является асинхронным, особенно, если тестируется система в процессе ее реальной работы

Резюмируя, еще раз отметим актуальность проблемы создания теории конформности, которая обладала бы следующими свойствами

1 могла применяться к широкому классу семантик взаимодействия, основанных на наблюдаемом поведении, с параметризацией конформности той или иной семантикой из этого класса,

2 учитывала в спецификации дивергенцию и запрещённое (не декларированное) поведение, допустимые в реализации, а не просто запрещала их;

3 была развита до уровня алгоритмов генерации тестов,

4 решала проблему монотонности - сохранения конформности при композиции, в частности, при асинхронном тестировании

Цели и задачи исследования

Целью диссертационной работы является создание теории конформности, обладающей указанными выше свойствами Достижение этой цели требует решения следующих задач

1. Формализация тестового эксперимента с целью определения семантики взаимодействия, основанной на наблюдаемом поведении и параметризуемой тестовыми возможностями по управлению и наблюдению Элементы такой семантики описывают управление и наблюдение и состоят из 1) действий, которые может выполнять реализация и которые наблюдаемы тестом, 2) кнопок, на которых «написаны» множества разрешаемых каждой кнопкой действий (элемент управления), 3) наблюдаемых отказов - для тех «кнопочных» множеств, для которых возможно наблюдение отсутствия какого бы то ни было действия. Параметризация должна обеспечиваться возможностью задания любых (но согласованных между собой) наборов таких элементов

2 Построение трассовой теории, в которой модель - это множество трасс наблюдений (действий и отказов) с ограничениями, вытекающими из семантики взаимодействия С целью внесения в теорию дивергенции и запрещённого поведения следует предусмотреть в спецификации возможность завершать такие трассы специальными действиями, моделирующими дивергенцию и запрещенное поведение (действие, называемое разрушением) Определение в рамках трассовой теории для заданной семантики взаимодействия следующих понятий 1) безопасное тестирование как тестирование, избегающее дивергенцию и разрушение в реализации, 2) гипотеза о безопасности реализации, определяющая класс безопасных реализаций, то есть реализаций, которые могут безопасно тестироваться для данной спецификации, 3) безопасная конформность, то есть конформность, учитывающая (помимо семантики взаимодействия) дивергенцию и разрушение, и для заданной спецификации определяющая класс конформных реализаций Разработка методов генерации наборов тестов по заданной трассовой спецификации в заданной семантике взаимодействия, обеспечивающих полноту тестирования Предлагаемые методы должны поддаваться алгоритмизации при достаточно слабых ограничениях на спецификацию

3 Построение ЬТБ-теории, включающей определение ЬТБ-модели, трасс наблюдений ЬТБ-модели, гипотезы о безопасности, безопасной конформности и (алгоритмизуемые) методы генерации тестов Кроме того, на уровне ГЛ^-теории определяется композиция моделей, которую невозможно определить в теории трасс наблюдений

4 Разработка (алгоритмизуемых) методов пополнения спецификаций, целью которого является переход к такой семантике взаимодействия, в которой наблюдаемы все отказы (для всех кнопок) При таком переходе должен обязательно сохраняться класс конформных реализаций, и желательно сохранение класса безопасных реализаций Этим, во-первых, достигается самоприменимость спецификации (она конформна сама себе), то есть

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

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

Методологическая и теоретическая основа исследования

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

Научная новизна исследования

Новым в диссертационной работе являются 1 Метод формализации тестового эксперимента с помощью параметризуемой машины тестирования, целью которого является определение семантики взаимодействия

а Отличие от машин Милнера и Ван Глаббека заключается в параметризации машины набором «множественных» кнопок. Это является способом задания семантики взаимодействия, основанной только на наблюдениях (не на соответствии состояний) и моделирующей тестовые возможности по управлению и наблюдению Впервые для таких семантик появляется возможность единообразно определять не только задаваемые

машинами Милнера и Ван Глаббека, но и многие другие, применяемые в теории и на практике, семантики, в частности, семантику отношения ioco Ъ Вводится новое понятие разрушения, означающее специальное действие, которое моделирует запрещенное и/или недекларированное поведение системы В отличие от рассматриваемого запрещённого состояния, разрушение, как запрещенное действие, может быть введено на уровне машины тестирования и в дальнейшем использовано в трассовой модели, а не только в модели LTS 2 На уровне трассовой и LTS-моделей вводятся взаимосвязанные концепции а Безопасное тестирование как тестирование, избегающее разрушения и не продолжающее тестовый эксперимент в том случае, когда возможна дивергенция Это является хорошей альтернативой полному запрету на дивергенцию и разрушение, что позволяет расширить домен отношения конформности.

b Гипотеза о безопасности - такая гипотеза о реализации, которая позволяет

безопасно тестировать ее для заданной спецификации с Безопасная конформность saco (safe conformance), которая позволяет декларировать в спецификации дивергенцию и разрушение, опирается на гипотезу о безопасности и параметризуется семантикой взаимодействия Многие частные конформности, основанные на семантиках наблюдаемого поведения (без учета состояний), такие как отношение ioco, можно рассматривать как частные случаи отношения saco 3. Метод генерации полного набора тестов для безопасной конформности по заданной спецификации, который является обобщением аналогичных методов для частных конформностей (в том числе, отношения ioco) и алгоритмизуем при достаточно слабых ограничениях на спецификацию В отличие от аналогичных методов спецификация может быть задана не только в форме LTS, но и в форме модели наблюдаемых трасс Кроме того, обеспечивается безопасное тестирование даже в тех случаях, когда в

реализации есть дивергенция и разрушение, при условии, что реализация удовлетворяет гипотезе о безопасности

4 Метод пополнения спецификаций, сохраняющего классы безопасных и конформных реализаций, с использованием специальных фиктивных действий «не-отказов» Этот метод позволяет перейти к семантике, в которой все отказы наблюдаемы и которая является отношением предпорядка (в частности, рефлексивна) Метод поддается алгоритмизации при достаточно слабых ограничениях на спецификацию. Частное применение этого метода решает проблему пополнения для семантики отношения loco.

5 Введение ф-трасс и соответствующей модели ф-трасс как промежуточного уровня абстракции между моделью наблюдаемых трасс, достаточной для определения конформности, но не достаточной для определения композиции моделей, и уровнем LTS-моделей, где такая композиция определяется Эта модель позволяет в единой трассовой теории формализовать как конформность, так и композицию, что является ключевым моментом в проблеме монотонности В частности, по ф-модели восстанавливается модель наблюдаемых трасс, а композиция ф-моделей обладает важным свойством аддитивности ф-модель, соответствующая композиции LTS-моделей, совпадает с композицией ф-моделей, соответствующих LTS-операндам

6 Метод монотонного преобразования спецификаций для семантики, в которой все отказы наблюдаемы Этот метод позволяет сохранить при преобразовании классы конформных и безопасных реализаций, и применим в случае асинхронного тестирования Метод поддается алгоритмизации при дополнительных достаточно слабых ограничениях на спецификацию Частное применение этого метода решает проблему монотонности для семантики отношения toco

Практическая значимость работы

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

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

Разработка указанных алгоритмов и создание на их основе практических инструментов позволяет решать важнейшие практические задачи 1) генерацию полного набора тестов по спецификации и 2) генерацию спецификации системы по спецификациям компонентов Решение последней задачи, помимо получения спецификации системы как документа для ее пользователя и её

разработчика, позволяет 3) генерировать системные тесты по спецификациям компонентов и 4) верифицировать декомпозицию системных требований, то есть проверять согласованность заданных спецификаций компонентов и спецификации системы

Апробация результатов исследования

Теория конформности, предлагаемая в диссертационной работе, создавалась в результате осмысления и обобщения практического опыта тестирования на основе формальных моделей, которое проводилось в ИСП РАН, начиная с 1994 г Многие основные идеи, понятия и методы, предложенные в работе, находили свое применение в создании и дальнейшем развитии тестовых систем KVEST (Kernel VEnfication and Specification Technology) и UniTESK (Unified TEstmg & Specification Toolkit) В первую очередь это относится к понятиям разрушения и безопасного тестирования, а также к преобразованиям спецификации при асинхронном тестировании с различными средами передачи

Результаты диссертационной работы были доложены на следующих Российских и международных научных конференциях и семинарах

Всероссийская научная конференция "Научный сервис в сети интернет технологии распределенных вычислений", Абрау-Дюрсо, 2005,

• Семинар Института проблем информационной безопасности при МГУ им М.В Ломоносова, 2005 г,

Европейская объединенная конференция по теории и практике программного обеспечения ETAPS, семинар «Тестирование на основе моделей», Вена, Австрия, 2006 г;

• Пятая общероссийская научная конференция «Математика и безопасность информационных технологий» (МаБИТ-06) в рамках Международной

научной конференции по проблемам безопасности и противодействия терроризму, Москва, 2006 г,

Семинар кафедры математической кибернетики ф-та ВМиК МГУ им М.В Ломоносова, Москва, 2006г,

Семинар «Тестирование дискретных управляющих систем на основе автоматных моделей», Томский Государственный Университет, 2006 г, Научный семинар «Проблемы современных информационно-вычислительных систем», мех-мат фак-т МГУ им MB. Ломоносова, Москва, 2006 и 2007 г г

По тематике диссертационной работы автор участвовал в выполнении следующих грантов РФФИ

96-01-01277-а «Методы тестирования программного обеспечения на основе формальных спецификаций» (1996-1998);

• 99-01-00207-а «Формальные методы в форвард- и реверс-инженерии программных систем» (1999-2001);

02-01-00959-а «Повторное использование формальных спецификаций в производстве и тестировании программных систем» (2002-2004),

• 04-07-90308-в «Верификация функций безопасности и мобильности протоколов IP» (2004-2006),

05-01-00999-а «Методы формальных спецификаций в тестировании Интернет-приложений» (2005-2007), 07-07-00243-а «Верификация функций безопасности протокола нового поколения IPsec v2» (2007-2009). Содержание диссертационной работы легло в основу разработанного совместно с АС Косачевым учебного курса «Теория верификации соответствия программ», который читался на механико-математическом ф-те МГУ им М.В Ломоносова весной 2006 г Отдельные элементы теории используются в учебном курсе «Тестирование на основе моделей», который читается на ф-те ВМиК МГУ им M В Ломоносова, начиная с 2007 г и в курсе

«Методы формальной спецификации программ», который читался на 3-ем потоке ф-та ВМиК МГУ им М В Ломоносова в 1995-2007 г г

Публикации

По теме диссертационной работы опубликовано 27 работ, полностью отражающих основные научные результаты работы, в том числе 7 в рецензируемых научных изданиях по списку ВАК 2007 года

Структура и объём работы

Диссертационная работа состоит из введения, шести глав, заключения, списка литературы и приложения, содержащего доказательства утверждений, встречающихся в тексте Каждая глава разбита на разделы, некоторые разделы разбиты на подразделы, каждый уровень имеет независимую нумерацию внутри единицы вышестоящего уровня 135 определений, 84 леммы и 49 теорем имеют раздельную сквозную нумерацию по всему тексту Содержание работы изложено на 424 страницах (без приложения), список библиографических ссылок включает 154 наименования (для удобства пользования сначала перечисляются работы автора, затем другие работы на русском языке и, наконец, работы на других языках) В тексте содержится 72 рисунка

Содержание работы

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

Автор опирается на NBG (Нейман, Бернайс, Гедель) аксиоматическую теорию множеств с праэлементами Эта теория основана на понятиях класса и праэлемента Обычные теоретико-множественные операции и отношения (конструктор, объединение, пересечение, вложенность, декартовое произведение) определяются для класса, который считается состоящим из элементов. Такими элементами могут быть праэлементы и некоторые классы, называемые множествами Праэлемент - это объект, который является элементом класса, но сам классом не является Множество - это класс, который является как элементом другого класса, так и сам состоит из элементов (множеств и праэлементов) Собственный класс - это класс, который не является множеством, то есть не является элементом какого-либо класса, хотя сам состоит из элементов (множеств и праэлементов).

Собственными классами являются, в частности, различные классы LTS, поскольку не налагается никаких ограничений на множество состояний отдельной LTS Если бы такие классы считались множествами, это привело бы к тем или иным вариантам известных парадоксов наивной теории множеств Например, в третьей главе диссертации определяется объединение множества LTS с помощью введения нового состояния, из которого проводятся внутренние переходы в начальные состояния LTS-операндов Показывается, что объединение некоторого множества конформных LTS также конформно Однако, если объединять все конформные LTS, то такое объединение является собственным операндом, что приводит к бесконечной цепочке внутренних переходов, то есть дивергенции А наличие дивергенции в самом начале неконформно для большинства спецификаций, что противоречит конформности объединения

С той же целью обхода этих парадоксов иногда вместо «система» говорят «пространство» (labeled transition space), а для задания отдельной LTS указывают ее начальное состояние как одно из состояний LTS-пространства Однако в этом случае возникают трудности при определении различных преобразований LTS

Под деревом последовательностей понимается множество последовательностей, замкнутое по операции взятия префикса последовательности Под порождающим графом понимается граф с выделенными начальными и конечными вершинами, дуги которого могут быть помечены символами из некоторого алфавита Граф порождает множество последовательностей в этом алфавите, которые являются последовательностями помеченных дуг маршрутов графа

Глава 2 посвящена формализации тестового эксперимента с целью определения семантики взаимодействия теста и реализации Рассматриваются различные тестовые возможности, задаваемые с помощью машины тестирования Среди них выделяется набор теоретически достаточно мощных и практически значимых возможностей, определяющих 9Я/£}-машину Эта

машина задает 5Н/£2-семантику тестирования, которая строится на

наблюдениях внешних действий и отказов.

Отличие от реактивной машины Милнера и генеративной машины Ван Глаббека заключается в том, что вместо нажатия одной или нескольких кнопок, каждая из которых соответствует одному разрешаемому действию, предлагается нажимать одну кнопку, которой соответствует множество таких действий Кроме того, для каждой кнопки указывается, соответствует ли ее «кнопочному» множеству наблюдаемый отказ (91-кнопки) или нет (О-кнопки).

Набор семейств подмножеств алфавита внешних действий ,

покрывающих весь алфавит (и£Н) и (и£1) =Ь, как раз и является параметром

машины, с помощью которого задается та или иная семантика Параметризация семействами наблюдаемых и ненаблюдаемых отказов позволяет учитывать те или иные ограничения на (правильное) взаимодействие Многие известные семантики тестирования оказываются вариантами £Н/£2-семантики при

соответствующем определении семейств Л и Q Например, семантика

отношения ioco для реактивной системы предполагает, что при тестировании можно посылать в реализацию один стимул, а принимать все реакции, отсутствие реакций (стационарность, традиционно обозначаемая символом 5) наблюдаемо, а блокировка стимула не наблюдаема Такую семантику автор предлагает называть 8-семантикой, она совпадает с *К/£2-семантикой, где £Н

состоит из одного множества всех реакций, а £} это множество блокировок

стимулов (блокировка стимула - это множество, состоящее только из этого стимула) Если запрещается торможение реакций, то при посылке стимула всегда одновременно принимаются все реакции, что означает множество из семейства £} это множество, состоящее из всех реакций и одного стимула И

так далее

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

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

независимо от других разрешенных и определенных действий Репликация означает «копирование» машины с независимым наблюдением ее поведения в разных копиях Если репликация допустима в любой момент времени, это дает возможность отслеживать состояния реализации (с точностью до их эквивалентности, как множество дальнейших поведений) и определять отношения конформности типа симуляций. В диссертационной работе такие возможности не рассматриваются, и предполагается, что репликация возможна только перед тестированием, что моделирует различные прогоны одного и того же или разных тестов Глобальное тестирование означает теоретическую возможность получить наблюдение любого возможного поведения реализации, что необходимо для полноты тестирования Бесконечные наблюдения не рассматриваются, поскольку они практически не реализуемы и избыточны для отношений конформности, основанных на конечных трассах наблюдений (тесты заканчиваются через конечное время) Отрицательное наблюдение «вычисляется» по множеству всех наблюдений Например, если после трассы ни разу не наблюдалось действие из отказа Р, то трасса продолжается отказом Р Однако, это ничего нового не дает, если соблюдён принцип независимости поведения реализации и нет репликации в любой момент времени Поэтому отрицательные наблюдения в работе не рассматриваются

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

Глава 3 содержит теорию трасс наблюдений Определяется модель наблюдаемых трасс (£Н-трасс) для заданной £Н/£3-семантики взаимодействия,

которые состоят из действий и SH-отказов и могут заканчиваться дивергенцией

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

Вводится полная трассовая модель (/^-модель), соответствующая семантике, в которой любому подмножеству внешних действий соответствует своя £Н-кнопка Показывается, что проекция полной модели на SH-трассы

является *Н-моделью, и любая SH-модель является проекцией полной модели

Доказывается утверждение о разложении F-модели на, так называемые, стабильные и контрстабильные деревья, что соответствует состояниям LTS и в следующей главе используется для установления эквивалентности трассовой и LTS-теорий с точки зрения конформности

В этой главе показано, что трассовая теория достаточна для формулировки отношений безопасности и безопасной конформности Определяются отношения безопасности в реализации safe in и в спецификации safe by, означающие «кнопка безопасна после трассы» На этой основе определяются безопасные трассы реализации Sufeiit (I) и спецификации SafeE>y(E).

Гипотеза о безопасности - это отношение safe for — «реализация безопасно-тестируема для спецификации» 1) если спецификация не разрушается с самого начала, то и реализация не разрушается с самого начала, 2) после трассы, которая безопасна как в реализации, так и в спецификации, кнопка, безопасная в спецификации, должна быть безопасна в реализации

I safe for £ =def ((y)gS => <y)gl) & VaeSafeBy (£) rSafeln (I)

VPeíHuQ {P safe by £ after a => P sa/e in I a/Cer a).

Безопасная конформность saco - <феализа1щя безопасно-конформна спецификации» - применима только к безопасным реализациям и означает любое наблюдение, которое возможно над реализацией, возможно в спецификации в той же самой безопасной ситуации, то есть после общей безопасной трассы при нажатии кнопки, безопасной в спецификации I saco £ =def I safe for I & VceSafeBy (2) nSafeln (I)

VP safe by £ after a obs (a, P, I) cobs (a, P,£), где obs означает множество возможных наблюдений, когда после трассы ст нажимается кнопка Р.

Для конформности saco определяется понятие трассового теста и выясняются условия конечности времени выполнения теста Также введено понятие управляемого (без лишнего недетерминизма) теста Далее на трассовом уровне определено отношение «реализация проходит тест», значимые, исчерпывающие и полные наборы тестов. Выделен подкласс строгих тестов (найденная ошибка всегда фиксируется) и доказано утверждение о полном наборе строгих управляемых тестов Для примитивных тестов, каждый из которых строится ровно по одной безопасной трассе спецификации, этот набор содержит только ограниченные (по времени выполнения) управляемые строгие тесты После этого рассматриваются вопросы оптимизации (редукции) тестов и набора тестов, которые могут использоваться на практике Глава завершается кратким рассмотрением вопроса об алгоритмическом задании трассовой модели и алгоритмической генерации полного тестового набора Метод генерации полного набора тестов для безопасной конформности по заданной спецификации является обобщением аналогичных методов для частных конформностей (в том числе, отношения ioco) Отличие, во-первых, в том, что спецификация может быть задана в виде модели наблюдаемых трасс, а не в виде LTS, и, во-вторых, в том, что обеспечивается безопасное тестирование

даже, если в реализации есть дивергенция и разрушение, при условии, что реализация удовлетворяет гипотезе о безопасности

В главе 4 в качестве модели рассматривается система помеченных переходов (ЬТ8) Новым является введение перехода по разрушению. Трассы ОБ - это трассы ее маршрутов, причём при проходе стабильного состояния в трассу может добавляться любая конечная последовательность $Н-отказов,

соответствующих состоянию (отказ как множество действий, по которым нет переходов из состояния). Дивергенция как бесконечная цепочка т-переходов, которой продолжается маршрут, допускается в ЬТБ и моделируется А-действием в конце трассы маршрута Устанавливается эквивалентность трассовой и ЬТв-моделей в том смысле, что множество трасс наблюдений, задаваемых ЬТБ, является моделью наблюдаемых трасс, и каждая модель наблюдаемых трасс может быть задана некоторой ЬТБ Это позволяет развить ЬТБ-теорию, опираясь на трассовую теорию определить гипотезу о безопасности и безопасную конформность С точки зрения безопасности, конформности и генерации тестов ЬТБ-модель более «избыточна», чем трассовая модель Однако она имеет ряд преимуществ.

ЬТЭ-модель более наглядна и удобна для человеческого восприятия Многие вещи можно увидеть в ней, так сказать, непосредственным созерцанием (когда пишут, что это «очевидно») Трассовая модель не обладает такой наглядностью. В частности, генетическое определение 91-трасс через

ЬТ8 просто и понятно, а интенсиональное определение -¡Н-модели более

сложно и далеко не очевидно ЬТБ более естественно «укладывается» в чёрный ящик машины тестирования, чем трассовая модель.

Но самым главным преимуществом ЬТ8-модели является возможность определения композиции составной модели из моделей-компонентов, используя оператор параллельной композиции алгебры процессов (в данной

работе оператор Ц. аналогичный оператору композиции в CCS - (Calculus of

Communicating Systems) Соответственно, взаимодействие в LTS-теории выглядит как композиция LTS-реализации и LTS-окружения, а тестирование — как композиция LTS-реализации и LTS-теста С этой точки зрения £Н/£3-

машина тестирования интерпретируется как ограничение на LTS-окружение/тест, то есть на способ (правильного) взаимодействия с LTS-реализацией

Для того, чтобы метод генерации трассовых тестов можно было использовать для генерации LTS-тестов, во-первых, показывается соответствие отношений «реализация проходит тест» в трассовой и LTS-теориях, и, во-вторых, определяется преобразование трассового теста в LTS-тест

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

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

Сначала проблема пополнения рассматривается для частного случая 8-семантики и отношения юсо, отличающегося от отношения ioco$ (saco в 8-семантике) только более узким доменом реализаций и спецификаций Показано, что отношение ioco, вообще говоря, нерефлексивно, транзитивно и немонотонно Также для 8-семантики существует проблема выхода за пределы домена отношения ioco (и ioco¿) при композиции (возникновение дивергенции как бесконечной цепочки синхронных переходов). Эта проблема решается в предлагаемом отношении ioco^ {saco в у8-семантике, то есть 8-

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

Далее исследован вопрос о рефлексивности и транзитивности конформности, и определяется необходимое и достаточное условие рефлексивности и достаточное условие транзитивности Показано, что при отсутствии £2-кнопок (ненаблюдаемых отказов) эти условия выполнены и в

íH/0-семантике отношение saco является предпорядком

Наконец, доказывается существование пополнения, сохраняющего класс конформных реализаций и такого, что для пополненной спецификации классы конформных реализаций в JH/Ü2- и SHujQ/0-семантиках совпадают Это

пополнение строится как объединение конформных трассовых реализаций

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

причины сужения класса безопасных реализаций и предложено решение проблемы, основанное на введении фиктивных действий - не-отказов С помощью не-отказов удается сделать такое пополнение, которое сохраняет не только конформные, но и безопасные реализации Кратко рассмотрены вопросы алгоритмизации этого пополнения и его частные случаи для 8-, уб- и (Зу8-семантик (последняя допускает блокировки стимулов)

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

Ii saco Si & I2 saco S2 =£> Ii1|.I2 saco Si1|.S2

Поскольку с помощью пополнения спецификации можно перейти к семантике без 0-кнопок с сохранением классов безопасных и конформных

реализаций, в данной главе рассматриваются только семантики без 0-кнопок,

когда конформность saco является предпорядком

Для решения проблемы монотонности создана общая теория монотонности, в рамках которой вводятся следующие понятия Корректная спецификация системы - это такая спецификация, которая удовлетворяет условию монотонности прямая композиция компонентов, конформных своим спецификациям, конформна спецификации системы Ii saco Sx & l2 saco S2 => I1Ul2 saco S

Далее определяется специальная - косая - композиция спецификаций компонентов S!//S2 как самая сильная (предъявляющая наибольшие

требования к реализации) корректная спецификация системы, разумеется, в предположении, что такая самая сильная корректная спецификация существует

Решение проблемы монотонности предложено искать как монотонное преобразование % обладающее тем свойством, что косая композиция спецификаций совпадает с прямой композицией монотонных (монотонно преобразованных) спецификаций Si//S2 = tf"(Si) \[T{S2)

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

семантике и LTS-моделями В частности, для ф-трасс определяется оператор композиции Сформулированы восемь достаточных условий монотонности Шесть из них не связаны с самим монотонным преобразованием, и описывают связь между конформностью saco, трассами наблюдений (fH-трассами), ф-

трассами и оператором прямой композиции Ц Два условия налагаются на

преобразование для того, чтобы оно было монотонным

Для SH-трасс определено отношение мажорирования и доказано его

эквивалентность конформности (первое условие монотонности)

ф-трассы аналогичны 5Н-трассам, но вместо 5Н-отказа в стабильном

состоянии s в трассу может быть добавлен ф-символ состояния как пара (ref-множество, gamma-ыпожество), где /■¿¿•множество - состоит из действий, по которым нет переходов из s, а ga/и/ия-множество - из действий, после перехода по которым есть переход по разрушению Кроме того, рассматриваются не только конечные, но и бесконечные ф-трассы Для ф-трасс определяется оператор их композиции, дающий множество ф-трасс

Для ф-трасс доказаны два условия монотонности. 1) Генеративность по ф-трассам модели однозначно восстанавливаются ее ÍH-трассы 2) Аддитивность

множество ф-трасс композиции LTS совпадает с объединением композиций ф-трасс LTS-операндов Ф® (SiH.S2) =и (Фш (SJ ЦФЮ (S2) ), где оператор Фю дает множество ф-трасс LTS Первое свойство дает возможность учитывать

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

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

Остальная часть главы посвящена поиску меньших по объему монотонных подмоделей Для этого вводится отношение мажорирования ф-трасс,

отвечающее двум важным условиям 1) Генеративность мажорирование ф-трасс влечет мажорирование генерируемых ими !Н-трасс 2)

Композиционность мажорирование ф-трасс операндов влечет мажорирование ф-трасс композиции Ф® (I!) (81) и Ф® (12) (Б2) влечет

и (Фга (I!) ЦФ® (12) ) ^и(Ф'!>(31) Ц.ФЮ (82) ) Также показано, что

мажорирование ф-трасс является предпорядком

Такое отношение мажорирования позволяет удалить из наибольшей монотонной спецификации «лишние» ф-трассы, если они мажорируются оставшимися ф-трассами К сожалению, далеко не всегда можно получить наименьшую (и даже минимальную) монотонную спецификацию Предложены три вложенные монотонные подмодели

Соп/( Э) э финальная 2 однородная э сингулярная.

К сожалению, сингулярная монотонная подмодель Т(3) наибольшей монотонной спецификации Соп/( Э) не всегда существует Для ее существования налагаются ограничения на ветвимость исходной ЬТ8-спецификации Б Спецификации, удовлетворяющие этим ограничениям названы конечно-доминируемыми Частично эти ограничения совпадают с тестовьми ограничениями, то есть ограничениями, требуемыми для алгоритмической генерации тестов по исходной спецификации Б Дополнительные ограничения нужны для того, чтобы преобразованная сингулярная модель также удовлетворяла тестовым ограничениям, то

есть чтобы по ней также можно было алгоритмически генерировать тесты Метод монотонного преобразования спецификаций поддается алгоритмизации при достаточно слабых ограничениях на спецификацию Частное применение этого метода решает проблему монотонности для отношения юсо

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

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

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

Решение второй задачи позволяет достигнуть три цели 1) Построенная спецификация системы может рассматриваться как описание системы с точки зрения ее пользователей 2) Такую спецификацшо можно считать техническим заданием для разработчика системы, в том числе, при возможных дальнейших модификациях системы (ее компонентов) с сохранением внешней функциональности и схемы компоновки 3) По спецификации системы можно генерировать системные тесты при дополнительных гипотезах о реализациях

Заключение

В настоящее время повышение качества, безопасности и надежности ПО, как вновь создаваемого, так и давно находящегося в эксплуатации, стала важнейшей проблемой как для разработчиков реальных программных систем в индустрии, так и для исследователей в области информатики Ключевой частью решения этой проблемы является тестирование программ, доля которого во времени и других ресурсах от общих расходов на разработку ПО составляет около 50%, а для критических по безопасности приложений - до 90% Противоречивая задача повышения качества программ и снижения затрат на тестирование диктует необходимость поиска путей автоматизации тестирования Одним из важнейших методов решения этой задачи является тестирование на основе формальных (математических) моделей, целью которого является проверка того, что реализационная модель (модель

тестируемой системы) соответствует (конформна) спецификации (модель требований)

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

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

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

возможности по управлению и наблюдению поведения реализации. Также вводится понятие разрушения, моделирующее запрещенное и/или недекларированное поведение системы

2 Введение на уровне трассовой и ЬТБ-моделей концепции безопасного тестирования, избегающего разрушения и не продолжающего тестовый эксперимент в том случае, когда возможна дивергенция Введение гипотезы о безопасности реализации, которая позволяет ее безопасно тестировать для заданной спецификации, и безопасной конформности, которая позволяет декларировать в спецификации дивергенцию и разрушение, опирается на гипотезу о безопасности и параметризуется семантикой взаимодействия

3 Метод генерации полного набора тестов для безопасной конформности по спецификации, заданной в виде модели наблюдаемых трасс или ЬТБ-модели, обобщающий аналогичные методы для некоторых частных семантик на произвольную семантику взаимодействия, основанную на наблюдаемом поведении Метод алгоритмизуем при достаточно слабых ограничениях на спецификации

4 Метод пополнения спецификаций с использованием специальных фиктивных действий «не-отказов», который позволяет сохранять класс безопасных реализаций и поддается алгоритмизации при достаточно слабых ограничениях на спецификацию В частности, решается проблема пополнения для семантики отношения юсо

5 Разработка концепции ф-трасс и модели ф-трасс, которые позволяют в единой трассовой теории формализовать как конформность, так и композицию, что является ключевым моментом в проблеме монотонности.

6 Метод монотонного преобразования спецификации, который при достаточно слабых ограничениях на исходную спецификацию строит монотонную спецификацию. Метод поддается алгоритмизации при достаточно слабых ограничениях на спецификацию. Частное применение этого метода решает проблему монотонности для семантики отношения юсо

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

Несколько слов следует сказать о перспективах дальнейшего развития теории конформности. Во второй главе уже были указаны два таких основных направления- 1) использование трасс готовности (ready traces) и соответствующей безопасной конформности resaco, 2) использование приоритетов

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

Использование приоритетов можно считать чрезвычайно важной и актуальной задачей ближайшего развития теории и практики конформности Это решило бы целый ряд проблем тестирования- 1) выход из дивергенции при наличии более приоритетного «задания» для реализации, в частности, при асинхронном тестировании реактивных систем выход из цикла осцилляции (бесконечной цепочки выдачи реакций) при поступлении стимула, 2) определение альтернативного поведения реализации при возникновении тупиков (6-переход в реализации), 3) проблема торможения реакций тестом в реактивных системах, 4) возможность для реализации распознавать отсутствие стимулов в реактивных системах (е-действие) и др

Важное значение имеет также развитие теории конформности в сторону специальных версий теории для ограниченных классов семантик, спецификаций и реализаций На этом пути за счет сужения области применимости можно получить большую эффективность Хотя это кажется возвратом к хаосу всевозможных моделей и конформностей, на самом деле этот процесс закономерен и упорядочен, поскольку идёт в рамках общей теории как ее конкретизация в частных случаях с сохранением единых понятий и методологии В частности, весьма многообещающим кажется соединение общей теории конформности с методами тестирования конечных автоматов (в последнее время также и ЬТБ), основанными на обходе графа переходов Также полезные результаты получаются в области асинхронного тестирования, когда рассматриваются специальные типы среды передачи, например, многоканальные входные и выходные очереди, очереди с приоритетами и т п По сути здесь применяются специальные разновидности монотонного преобразования спецификаций, ориентированные на класс сред Особенностью таких тестовых систем является преобразование спецификации и композиция со средой «на лету», в процессе тестирования

Последняя проблема, на которой хотелось бы остановиться, это проблема «разрыва» между явными моделями конечных автоматов или ЬТБ, обычно применяемыми в теории конформности, и тем формализмом, в котором часто на практике задаются спецификации В частности, если спецификации записываются в виде пред- и постусловий, то, хотя в основе такой спецификации лежит ЬТБ-модель, однако она задана неявно - как решение системы уравнений В некоторых случаях удается построить Ш^-модель спецификации в процессе самого тестирования, точнее, ту ее часть, которая оказывается необходима и достаточна для тестирования данной реализации Этот подход оказался весьма полезным и успешно применяется в системе ишТЕБК Дальнейшее развитие может быть связано с расширением области применимости этого подхода

Публикации автора по теме диссертации

1 Burdonov I, Kossatchev А, Petrenko А, Cheng S , Wong H Formal Specification and Verification of SOS Kernel. BNR/NORTEL Design Forum, June 1996

2 Баранцев А В., Бритвина E H, Бурдонов И Б , Косачев А С., Гоманюк С В., Демаков А В , Иванов А В , Максимов А В , Петренко А К., Сазанов Ю Л, Сортов А А, Стефанов В П, Сумар Г М Архитектура системы генерации и пропуска тестов. Вопросы кибернетики, Москва, 1998

3. Burdonov I., KossathcevA, Petrenko A, Galter D KVEST Automated Generation of Test Suites from Formal Specifications Proceedings of Formal Method Congress, Toulouse, France, 1999, LNCS, No 1708

4. Бурдонов И Б , Косачев А С, Демаков А В , Петренко А К, Максимов А В Формальные спецификации в технологиях обратной инженерии и верификации программ Труды Института системного программирования РАН, No 1,1999

5 Бурдонов И Б , Косачев А С , Кулямин В.В. Использование конечных автоматов для тестирования программ «Программирование» 2000 No 2

6 Bourdonov IВ , Kossatchev A S , Petrenko A.K, Kuliamin V V Experiences in using testmg tools and technology m real-life applications. Proceedings of SETT'01, India, Pune, 2001

7 Burdonov I, Kossatchev A, Demakov A, Jarov A, Petrenko A, Kuliamm V , Zelenov S Java specification extension for automated test development. Proc of Andrei Ershov Fourth International Conference Perspectives of System Informatics (preliminary proceedings) Novosibirsk 2001

8. Burdonov I., Kossatchev A, Demakov A, Jarov A, Petrenko A, Kuliamm V, Zelenov S Java Specification Extension for Automated Test Development Proceedings of 4-th Intl Conf on Perspectives of System Informatics, LNCS 2244, Sprmger-Verlag, 2001

9 Bourdonov IВ , Kossatchev A.S , Petrenko А К, Kuliamin V V UmTesK Test Suite Architecture Proceedings of 11-th Symposium on Formal Methods Europe, LNCS 2391, Springer-Verlag, 2002.

10 БурдоновИБ, КосачевАС, КуляминВВ Асинхронные автоматы классификация и тестирование Труды ИСП РАН, т 4, 2003

11 Бурдонов И Б , Косачев А С, Кулямин В.В Неизбыточные алгоритмы обхода ориентированных 1рафов Детерминированный случай «Программирование» 2003 No 5

12 Кулямин В.В, Петренко А.К., Косачев A.C., Бурдонов И.Б Подход UmTesK к разработке тестов «Программирование», 2003, No 6

13 Kuliamin V V , Kossatchev A S , Petrenko А К, Pakoulin N V , Bourdonov I.B. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems Perspectives of System Informatics // LNCS No. 2890, SpringerVerlag, 2003

14. Bourdonov I, Kossatchev A, Kuliamm V, Petrenko A UniTesK. Model Based Testing in Industrial Practice. Proc of 1-st European Conference on Model-Driven Software Engineering, Nürnberg, December 2003

15 БурдоновИБ, КосачевАС, КуляминВВ Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай «Программирование» 2004 No 1

16 БурдоновИБ Обход неизвестного ориентированного графа конечным роботом. «Программирование», 2004, No 4

17 БурдоновИБ Проблема отката по дереву при обходе неизвестного ориентированного графа конечным роботом «Программирование», 2004, No 6.

18 Бурдонов И Б Исследование одно/двунаправленных распределенных сетей конечным роботом Труды Всероссийской научной конференции "Научный сервис в сети ИНТЕРНЕТ" 2004

19 Баранцев А В , Бурдонов И.Б , Демаков А В , Зеленов С В , Косачев А С, Кулямин В В., Омельченко В А, Пакулин Н В , Петренко А К,

ХорошиловАВ Подход UmTesK к разработке тестов: достижения и перспективы Труды ИСП РАН, т 5,М ИСП РАН, 2004

20 Бурдонов И Б , Косачев А С, Кулямин В В Мета-модель функциональной спецификации распределенной системы, пригодная для тестирования Труды Всероссийской научной конференции "Научный сервис в сети ИНТЕРНЕТ" 2004

21. Бурдонов И.Б, Косачев А С Тестирование компонентов распределенной системы. Труды Всероссийской научной конференции «Научный сервис в сети ИНТЕРНЕТ», Изд-во МГУ, 2005

22 Бурдонов И Б, Косачев А С Верификация композиции распределенной системы Труды Всероссийской научной конференции «Научный сервис в сети ИНТЕРНЕТ», Изд-во МГУ, 2005

23 Bourdonov I, Kossatchev А, Kuliamin V. Formal Conformance Testing of Systems with Refused Inputs and Forbidden Actions Proc Of МВТ 2006, Vienna, Austria, March 2006

24 Бурдонов И Б , Косачев А С., Пономаренко В Н, Шнитман В 3 Обзор подходов к верификации распределенных систем ИСП РАН, препринт 16, М, 2006

25 Бурдонов И Б , Косачев А С, Кулямин В В Формализация тестового эксперимента «Программирование», 2007, No 5.

26. Бурдонов И Б, Косачев А С, Кулямин В.В Безопасность, верификация и теория конформности Материалы Второй международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МНЦМО, 2007

27. Бурдонов И Б., Косачев А С, Кулямин В В Теория соответствия для систем с блокировками и разрушением «Наука», 200?

Напечатано с готового оригинал-макета

Издательство ООО "МАКС Пресс" Лицензия ИД N00510 от 01 12 99 г Подписано к печати 24 01 2008 г Формат 60x90 1/16 Услпечл 2,0 Тираж 100 экз Заказ 021 Тел 939-3890 Тел./факс 939-3891 119992, ГСП-2, Москва, Ленинские горы, МГУ им MB Ломоносова, 2-й учебный корпус, 627 к