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




НазваниеФормальные спецификации в технологиях обратной инженерии и верификации программ
страница1/5
ТипДокументы
rykovodstvo.ru > Руководство эксплуатация > Документы
  1   2   3   4   5

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

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

Труды Института системного программирования РАН, 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
  1   2   3   4   5

Похожие:

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

Формальные спецификации в технологиях обратной инженерии и верификации программ iconЛитература 1 Основная литература Основы генетической инженерии и биотехнологии
Основы генетической инженерии и биотехнологии / под ред. Ю. А. Горбунова. – Ивц минфина, 2010. – 288 с

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

Формальные спецификации в технологиях обратной инженерии и верификации программ iconДиссертация тема: «Комплексная информационная система, предназначенная...
Тема: «Комплексная информационная система, предназначенная для верификации моделей конвективных облаков»

Формальные спецификации в технологиях обратной инженерии и верификации программ iconИзвещение о заключении Спецификации А4 с единственным контрагентом на оказание услуг
Заключение Спецификации А4 с единственным контрагентом на оказание услуг по установке, настройке и эксплуатации оборудования и средств...

Формальные спецификации в технологиях обратной инженерии и верификации программ iconКодекс этики и профессиональной деятельности в области программной инженерии (версия 2)

Формальные спецификации в технологиях обратной инженерии и верификации программ iconДля участия в запросе предложений в один этап на поставку квадроциклов (снегоболотоходов)
По качеству – согласно прилагаемой спецификации и технического задания Товар поставляется в комплектности, согласно Спецификации,...

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

Формальные спецификации в технологиях обратной инженерии и верификации программ iconПозиция: soc asic руководитель проекта
Отладка Library Design Kit: Тестирование и установка маршрута разработки. Чип для верификации стандартных библиотечных ячеек. Функциональная...

Формальные спецификации в технологиях обратной инженерии и верификации программ iconТехническое задание на проведение конкурентной процедуры поставки...
Шкафы пр8703,ПР8503, кру-рн, выключатели врн-200 согласно спецификации или эквивалент

Формальные спецификации в технологиях обратной инженерии и верификации программ iconИнструкция по эксплуатации музыкального центра фирмы philips
Табличка с указанием рабочего напряжения, расположена на обратной стороне устройства

Формальные спецификации в технологиях обратной инженерии и верификации программ iconОбразовательная программа по реализации дополнительных образовательных программ
Образовательная программа по реализации дополнительных общеобразовательных программ – дополнительных общеразвивающих программ (далее...

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

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

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

Формальные спецификации в технологиях обратной инженерии и верификации программ iconИнструкция Цифровая фоторамка «мини»
С обратной стороны рамки снимите крыжку и вставьте батарейки. Включится экран и появится настройка Часов. Исходная дата 1 Января...


Руководство, инструкция по применению






При копировании материала укажите ссылку © 2018
контакты
rykovodstvo.ru
Поиск