Формальные спецификации в технологиях обратной инженерии и верификации программ
|
Скачать 2.21 Mb.
|
   И.Б.Бурдонов, А.С.Косачев, А.В.Демаков, А.К.Петренко, А.В.Максимов.Формальные спецификации в технологиях обратной инженерии и верификации программ. Труды Института системного программирования РАН, 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 Основная литература Основы генетической инженерии и биотехнологии Основы генетической инженерии и биотехнологии / под ред. Ю. А. Горбунова. – Ивц минфина, 2010. – 288 с |
|
Автомобильная система охраны нового поколения с обратной связью и... Кроме того, команды, посланные с любого из брелков прописанных в память сигнализации, будут приняты брелком с обратной связью при... |
|
Предварительные технические спецификации Предметом настоящей спецификации является графический tft lcd с пользовательским интерфейсом в виде панели с сенсорным экраном, используемой... |
|
Диссертация тема: «Комплексная информационная система, предназначенная... Тема: «Комплексная информационная система, предназначенная для верификации моделей конвективных облаков» |
|
Предлагаемые к рассмотрению в ходе проектирования технологические... Описание предлагаемой структуры подсистемы сбора, хранения и верификации данных 8 |
|
Кодекс этики и профессиональной деятельности в области программной инженерии (версия 2) |
|
Извещение о заключении Спецификации А4 с единственным контрагентом на оказание услуг Заключение Спецификации А4 с единственным контрагентом на оказание услуг по установке, настройке и эксплуатации оборудования и средств... |
|
Для участия в запросе предложений в один этап на поставку квадроциклов (снегоболотоходов) По качеству – согласно прилагаемой спецификации и технического задания Товар поставляется в комплектности, согласно Спецификации,... |
|
Теоретические вопросы: Общая характеристика организационных звеньев... Формальные организационные звенья. Типы строения формальных организационных звеньев |
|
С одной стороны, и Открытое акционерное общество «Завод «Буревестник»,... Заказчик оплатить и принять оригинальные картриджи (драм-картриджи;чипы) их заправку и восстановление (далее Услуги) по наименованию,... |
|
Доклад о ходе реализации и оценке эффективности муниципальных Программ... Программ, представленных администраторами Программ в соответствии с Порядком разработки, реализации и оценки эффективности муниципальных... |
|
Позиция: soc asic руководитель проекта Отладка Library Design Kit: Тестирование и установка маршрута разработки. Чип для верификации стандартных библиотечных ячеек. Функциональная... |
|
Техническое задание на проведение конкурентной процедуры поставки... Шкафы пр8703,ПР8503, кру-рн, выключатели врн-200 согласно спецификации или эквивалент |
|
Инструкция по эксплуатации музыкального центра фирмы philips Табличка с указанием рабочего напряжения, расположена на обратной стороне устройства |