Microsoft Word petrenko rus doc



Yüklə 332,91 Kb.
səhifə1/3
tarix08.08.2018
ölçüsü332,91 Kb.
#61155
  1   2   3

И.Б.Бурдонов, А.С.Косачев, А.В.Демаков, А.К.Петренко, А.В.Максимов.

Формальные спецификации в технологиях обратной инженерии и верификации программ.

Труды Института системного программирования РАН, N 1, 1999, стр. 35-47.

16 стр.


___________________________________________________________________

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

Аннотация

KVEST (Kernel Verification and

др.
В контексте индустриальной разработки




Specification Technology) – технология спецификации и верификации программного обеспечения, основанная на автоматизированной генерации тестов из формальных спецификаций. Эта технология была разработана в рамках контракта с Nortel Networks и базируется на опыте, полученном в результате академических исследований. К 1999 году методология и набор инструментов применялись в трех индустриальных проектах верификации телекоммуникационного ПО. Первый проект, The Kernel Verification project, дал название методологии и набору инструментов. Результаты этого проекта присутствуют в Formal Method Europe Application database [28]. Это одно из крупнейших приложений формальных методов, присутствующих в базе данных. Данная статья содержит краткое описание подхода, сравнение со сходными работами и перспективы развития*.
1. Введение
1.1 Обратная и прямая инженерия ПО

Задачи программной инженерии (software engineering) условно можно разделить на две большие группы – реверс- или обратная инженерия и форвард- инженерия (reverse- and forward- engineering). Разные исследователи и практические разработчики программного обеспечения (ПО) уделяют этим группам разную долю внимания, однако сейчас уже ни одна промышленная разработка не может игнорировать проблемы каждой из этих групп. Форвард-инженерия необходима для того, чтобы поддерживать поступательное развитие ПО, реверс- инженерия необходима для поддержки преемственности функциональности и таких характеристик как надежность, управляемость, открытость к изменениям и



* Часть работ по развитию методологии была выполнена в рамках грантов РФФИ

96-0101277 и 99-01-00207.

и развития ПО важно объединение методов


ориентированных

(ОО) языков

и

соответствующих

компиляторов

и




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

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

В данной статье "реверс-инженерия"

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





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

1.2 Формальные методы в разработке ПО

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

Формальные методы в программировании, по-видимому, появились практически одновременно с самим программированием. Из результатов советской программистской школы наибольшую известность получили работы А.А.Маркова (алгоритмы Маркова) [24] и работы А.А.Ляпунова [25] и его учеников (например, схемы Янова [26]). В более поздние годы много внимания формальным методам в СССР уделялось в работах киевских, новосибирских, ленинградских и московских ученых. Наиболее известной и распространенной формальной нотацией является нотация Бэкуса-Наура, использующаяся для описания синтаксиса формальных языков. Затем можно назвать машину Тьюринга, конечные автоматы (Finite State Machine – FSM or Finite Automata – FA), сети Петри, языки описания взаимодействующих процессов К.А.Хоара (C.A.Hoar) и Р.Милнера (R.Milner) и др.

По естественным причинам практически все работы по формальным методам были нацелены на форвард-приложения. В

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

В 70-е годы появились языки формальных спецификаций, которые с одной стороны имели много общего с языками программирования, а с другой стороны предоставляли специальные средства, сближающие их с математической нотацией и облегчающие рассуждения о свойствах таких формальных текстов. В качестве наиболее известных упомянем CSP [13], CSS [14], VDM [15], SDL[16], LOTOS [17].

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

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





работы, связанные с разработкой и анализом формальных спецификаций. Вместе с тем, на отдельных направлениях формальные методы и, в частности, языки формальных спецификаций достигли значимых успехов. Эти успехи, с одной стороны, были обусловлены удачным сочетанием потребностей предметной области и возможностей формальных методов (в первую очередь это проблемы описания телекоммуникационных протоколов; SDL, LOTOS – примеры языков спецификаций, использующихся в этих областях), и с другой стороны, приближением языков спецификации к формам, привычным в традиционном программировании (в первую очередь это Венский метод – Vienna Development Method – VDM и его развитие – языки Z и RAISE).

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

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

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

Программный контракт описывает синтаксис и семантику интерфейсов систем. Как правило, этот термин используется по

отношению к так называемым

"интерфейсам прикладных программ" (Application Program Interfaces – API). API – это интерфейс, который предоставляется сущностями, составляющими программу, например, процедурами, функциями, методами ОО классов и т.п.

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

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

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





формальны, то они могут рассматриваться как "машинно-читаемые". Тем самым появляется предпосылка полностью автоматизировать как генерацию тестов, так и анализ результатов тестирования.

Серьезным направлением в использовании формальных методов в последние десять лет стала “проверка

моделей” (model checking). Этот подход

демонстрирует компромисс между идеальной мечтой о верификации формальной системы и реальной практикой разработки ПО. Суть похода состоит в построении модели реальной системы и по возможности полной проверке корректности данной модели. Проверка, если возможно, проводится аналитическими методами. Если это невозможно, производится тестирование модели. При этом сложность модели, как правило, выбирается таким образом, чтобы была возможность провести “исчерпывающее” тестирование (exhaustive testing). Слабое место данного подхода – это проблемы построения модели и доказательство того, что модель достаточно содержательна, чтобы на основании модели можно было судить о свойствах реальной системы.

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

функциональности, так и масштабов их использования.


2. История и основные идеи

KVEST
2.1 История разработки и использования KVEST

В 1994 году Nortel Networks (предыдущие названия: Bell-Northern Research, Northern Telecom и Nortel) предложил ИСП РАН разработать методологию и комплект инструментов автоматизации тестирования интерфейсов прикладных программ (Application Program Interface – API). Первым практическим применением методологии стало ядро операционной системы реального времени. Был строго описан программный контракт ядра ОС и созданы тестовые наборы для проверки выполнения реализацией программного контракта.

В случае успеха проекта Nortel получал возможность автоматизированной проверки соответствия программному контракту следующих версий ядра. Кроме того, появлялась возможность улучшить структуру программного продукта в целом, поскольку во время определения программного контракта ИСП предложил установить минимальное и ортогональное множество интерфейсов ядра ОС.

ИСП организовал совместную группу исследователей и разработчиков. Члены

группы имели богатый опыт в разработке

операционных систем, систем реального времени, компиляторов и в использовании формальных спецификаций для систематического подхода к разработке и тестированию ПО [2, 9, 10].

За первое полугодие ИСП предложил первую версию интерфейсов ядра (Kernel Interface Layer – KIL) и произвел

сравнительный анализ доступных

методологий специфицирования. KIL был принят с незначительными модификациями. Наиболее подходящим языком спецификации был признан RSL (RAISE Specification Language) [11, 12].

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

прототипы спецификаций, разработан и

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





основные принципы анализа тестового покрытия. KVEST методология использует

модификацию СДНФ критерия для

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

За следующий год были созданы

окончательные версии спецификаций и инструментов для генерации и выполнения тестов. С середины 1996 до начала 1997 года почти все тестовые наборы были получены и ядро ОС успешно протестировано. Результаты тестирования оказались неожиданными для заказчика. Никто не думал, что в критической части ПО, используемого в этой области более десяти лет, будет обнаружено несколько десятков ошибок!



2.2 Основные идеи KVEST


В качестве

основного

метода

спецификации

используется

так




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

называемый "моделе-ориентированный" или "ориентированный на состояние" (model based or state based) подход. Этот подход является альтернативным к так называемому "алгебраическому" подходу, синонимами которого являются "аксиоматический" и "действие- ориентированный" (action based) подходы [21, 22]. В моделе-ориентированном подходе спецификация представляет собой привычную программистам совокупность функций и описаний данных, с которыми данные функции оперируют. Как правило, каждой операции (процедуре) целевой системы соответствует некоторая спецификационная функция. Со структурами данных картина существенно сложнее. Различаются "видимые" реализационные данные и скрытые. Видимыми всегда являются входные и выходные параметры операций (процедур, методов). Такие данные, как глобальные


СДНФ – совершенная дизъюнктивная нормальная форма.

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

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

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

Первый пример – это функция, которая выполняет некоторые арифметические вычисления над целыми числами. Известна



формула (одна из возможных), по которой выполняются данные вычисления, обозначим ее f(x), где x – аргументы. В таком случае эксплицитная спецификация целевой функции tf(x) будет иметь вид (X – тип аргументов; Y – тип результатов)

tf : X Y

tf(x) is f(x)

Имплицитная спецификация могла бы иметь следующий вид

post-tf : X × Y Boolean

post-tf(x, y) is y = f(x)

// здесь х – аргумент,

// а y – результат целевой функции

Заметим, что обе рассмотренные спецификации могут быть

реализационно-независимыми, поскольку мы не делаем никаких предположений о

том, по какой формуле выполняются вычисления в реализации целевой функции.

Важно лишь то, что результат целевой функции должен совпадать с результатом

вычисления по формуле f(x).

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

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

эксплицитную форму без дополнительных

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

post-tf : X × Y Boolean

post-tf(x, y) is abs(y-f(x)) < delta

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

независимыми лишь формально, а не по

существу. От хорошей спецификации, в

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

KVEST в полной мере использует этот прием описания программных контрактов с использованием абстрактных структур

данных. Это относится как к типам

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

В еще большей степени повышение уровня абстракции относится к описанию





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

Yüklə 332,91 Kb.

Dostları ilə paylaş:
  1   2   3




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2024
rəhbərliyinə müraciət

    Ana səhifə