Интегрированная методика автоматизированного построения формальных поведенческих моделей С-приложений по исходному коду

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

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

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

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

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

— определения базового инструмента для реализации метода автоматизированного построения формальных моделей С-приложений по исходному коду на основе анализа промышленных систем возвратного проектирования;

— определения эффективной формальной нотации для представления результатов возвратного проектирования на основе анализа нотаций, используемых в процессе промышленного производства ПО;

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

— разработки методик спецификации различных фрагментов С-кода приложений с помощью выбранной формальной нотации;

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

— проверки работоспособности предложенных методик и инструментальных средств в ряде учебных и промышленных проектов.

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

Методы исследования. Для решения поставленных в работе задач используются теории реактивных и традиционных систем, конечных автоматов и базовых протоколов, аппарат формальных спецификаций. Применяются стандарты языков Message Sequence Charts (MSC) и ANSI С. В основу исследований положен системный подход.

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

Научные результаты и их новизна.

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

2. Разработана методика структуризации представления модели, позволяющая проводить ее анализ по частям и на разных уровнях абстракции.

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

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

Апробация работы. Основные положения и результаты диссертационной работы докладывались и обсуждались на международных научных конференциях «Second Spring Young Researchers1 Colloquium on Software Engineering» (SPb, 2008), «Космос, астрономия и программирование» (СПб, 2008), Motorola Technology Day (SPb, 2006, 2007, 2008), «Технологии Microsoft в теории и практике программирования» (СПб, 2006, 2007, 2008, 2009), XXXVII неделя науки СПбГПУ (СПб, 2008).

Результаты, выносимые на защиту.

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

2. Методика структуризации представления модели, позволяющая проводить ее анализ по частям и на разных уровнях абстракции.

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

Публикации. Основные положения диссертации изложены в 9 печатных работах, в том числе в одной работе в журнале из перечня ВАК.

Внедрение. Разработанный подход внедрен в компаниях ЗАО «Моторола ЗАО», ООО «Эксиджен Сервисис» и ООО «ИЦ «Северо-Западная лаборатория» и использована при разработке учебно-методического комплекса СПбГПУ по курсу «Технологии программирования» на кафедре «Информационных и управляющих систем». Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.

Структура и объем работы. Диссертация состоит из введения, 4-х глав, заключения, списка литературы и 4-х приложений. Диссертация изложена на 142 страницах машинописного текста, содержит 124 рисунка, 19 таблиц, список литературы — 100 наименований.

Основные результаты, полученные в ходе выполнения работы:

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

2) На основе проведенного анализа формальных моделей были выделены три нотации (Basic protocols, SDL, UML), позволяющие описывать и отображать поведенческие и структурные свойства анализируемых систем на разных уровнях абстракции, а их инструментарий поддержки позволяет генерировать сценарии поведения моделей при исполнении.

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

4) Разработана и описана методика построения базовых протоколов по фрагментам С-кода.

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

6) Разработана и описана методика использования расширенных протоколов и протоколов-коннекторов для моделирования вызовов функций.

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

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

Разработанный метод автоматизированного построения формальных поведенческих моделей С-приложений был использован в компаниях ЗАО «Моторола ЗАО», ООО «Эксиджен Сервисис» и ООО «ИЦ «Северо-Западная лаборатория» в различных проектах. Анализ полученных результатов позволил установить, что автоматизированный подход по сравнению с ручным методом формализации обеспечивает:

— трехкратный выигрыш по трудозатратам при построении моделей, модифицируемых после построения;

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

Общий объем разработанного ПО, вошедшего в программный комплекс поддержки методики автоматизированной формализации С-приложений, составил около 100 килобайт исходного кода на языке Собъем документации на разработанное ПО — более 150 страниц.

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

Заключение

.

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

Для достижения цели в работе были решены следующие частные задачи:

1) Проведен анализ инструментальных средств возвратного проектирования, существующих в настоящее время на рынке ПО.

2) Проведен анализ наиболее распространенных формальных нотаций моделей программ.

3) Предложена и описана методика спецификации фрагментов С-кода базовыми протоколами.

4) На базе инструмента Klocwork Insight разработана программная реализация, позволяющая автоматизировать генерацию базовых протоколов по фрагментам С-кода, представляемого в виде абстрактных синтаксических деревьев.

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

6) Для подтверждения работоспособности предложенные методики и разработанный инструментарий программной поддержки применены в реальных программных проектах. Анализ результатов показал эффективность применения разработанной методики автоматизированного построения формальных поведенческих моделей.