Введение к работе
Актуальность работы. Использование формальных моделей приложений и средств их обработки на этапах промышленного производства и поддержки программного обеспечения (ПО) с каждым годом растет. Ключевым моментом здесь является адекватность модели и скорость ее построения, что во многом определяет качество анализа.
Эффективность решения задач этих этапов (верификация, восстановление документации и пр.) обеспечивается путем восстановления модели реализованной программной системы из исходного кода (возвратное проектирование, reverse engineering) и последующего ее анализа. Однако бывает, что объем восстановленных формальных спецификаций сопоставим с объемом исходных кодов системы. Кроме того, ценность полученного результата напрямую зависит от корректности и полноты модели, что требует активного участия специалистов предметной области с высокими требованиями к уровню их подготовки. Очевидно, что создание подобных спецификаций без применения автоматизированных средств- достаточно трудоемкая задача, снижающая эффективность практического использования формальных методов в промышленной разработке ПО.
В связи с этим, актуальной задачей является снижение трудоемкости построения формальных моделей приложений, обусловленная постоянным ростом объемов и увеличением сложности ПО современных программных систем.
Настоящая работа посвящена созданию автоматизированного подхода к построению формальных моделей С-приложений по исходному коду, пригодных для статического и визуального анализа поведенческих и структурных свойств. Подход основывается на представлении модели приложения в виде множества базовых протоколов, каждый из которых описывает элементарное событие в рамках его поведения. Для анализа модели используются графические диаграммы, отражающие поведенческие и структурные свойства приложения на заданном уровне абстракции, и автоматически сгенерированные сценарии, отражающие изменения в поведении модели. На основе сценариев проводится дальнейшая верификация реализованного приложения на соответствие исходным требованиям или фиксация извлеченных из программного кода знаний о его поведении.
Цели и задачи диссертационной работы. Целью диссертационной работы является разработка метода и инструментальных средств для автоматизированного построения формальных моделей С-приложений по исходному коду, пригодных для статического и визуального анализа поведенческих и структурных свойств. Для достижения цели в работе решены следующие задачи:
- определения базового инструмента для реализации метода автоматизированного
построения формальных моделей С-приложений по исходному коду на основе анализа промышленных систем возвратного проектирования;
- определения эффективной формальной нотации для представления результатов
возвратного проектирования на основе анализа нотаций, используемых в процессе промышленного производства ПО;
- определения модели поведения приложений на основе выбранной формальной
нотации, пригодной для статического и визуального анализа поведенческих и структурных свойств;
- разработки методик спецификации различных фрагментов С-кода приложений с
помощью выбранной формальной нотации;
- разработки программных средств, обеспечивающих автоматизацию построения
формальных моделей С-приложений по исходному коду;
- проверки работоспособности предложенных методик и инструментальных средств в
ряде учебных и промышленных проектов.
Предметом исследования являются методы и инструментальные средства, позволяющие автоматизировать построение формальных поведенческих моделей С-приложений по исходному коду.
Методы исследования. Для решения поставленных в работе задач используются теории реактивных и традиционных систем, конечных автоматов и базовых протоколов, аппарат формальных спецификаций. Применяются стандарты языков Message Sequence Charts (MSC) и ANSI С. В основу исследований положен системный подход.
Обоснованность и достоверность полученных результатов обеспечивается корректным использованием теорий реактивных и транзиционных систем, конечных автоматов и базовых протоколов; использованием аппарата формальных спецификаций; положительными итогами использования разработанных методик и программных средств в реальных проектах.
Научные результаты и их новизна.
Предложена формальная модель поведения приложений, реализованных на языке С, основанная на концепциях инсерционного программирования и пригодная для статического и визуального анализа поведенческих и структурных свойств.
Разработана методика структуризации представления модели, позволяющая проводить ее анализ по частям и на разных уровнях абстракции.
3. Разработана методика использования расширенных протоколов и протоколов-коннекторов для спецификации и моделирования вызовов функций и абстрагирования других фрагментов исходного кода, обеспечивающая сокращение размеров модели.
Практическая значимость работы. На базе полученных научных результатов разработан комплекс программных средств, предназначенный для автоматизированного построения формальных поведенческих моделей С-приложений по исходному коду. С помощью подобных моделей возможно проведение верификации ПО - сравнение исходных формальных спецификаций с восстановленными. Программный комплекс был использован в реальных проектах по разработке и поддержке ПО из разных областей.
Апробация работы. Основные положения и результаты диссертационной работы докладывались и обсуждались на международных научных конференциях "Second Spring Young Researchers' Colloquium on Software Engineering" (SPb, 2008), "Космос, астрономия и программирование" (СПб, 2008), Motorola Technology Day (SPb, 2006, 2007, 2008), "Технологии Microsoft в теории и практике программирования" (СПб, 2006, 2007, 2008, 2009), XXXVII неделя науки СПбГПУ (СПб, 2008).
Результаты, выносимые на защиту
Модель поведения приложений, реализованных на языке С, основанная на концепциях инсерционного программирования и пригодная для статического и визуального анализа поведенческих и структурных свойств.
Методика структуризации представления модели, позволяющая проводить ее анализ по частям и на разных уровнях абстракции.
Программные средства, обеспечивающие автоматизированное построение формальных моделей С-приложений по исходному коду.
Публикации. Основные положения диссертации изложены в 9 печатных работах, в том числе в одной работе в журнале из перечня ВАК.
Внедрение. Разработанный подход внедрен в компаниях ЗАО "Моторола ЗАО", ООО "Эксиджен Сервисис" и ООО "ИЦ "Северо-Западная лаборатория" и использована при разработке учебно-методического комплекса СПбГПУ по курсу "Технологии программирования" на кафедре "Информационных и управляющих систем". Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.
Структура и объем работы. Диссертация состоит из введения, 4-х глав, заключения, списка литературы и 4-х приложений. Диссертация изложена на 142 страницах
машинописного текста, содержит 124 рисунка, 19 таблиц, список литературы - 100 наименований.
Похожие диссертации на Интегрированная методика автоматизированного построения формальных поведенческих моделей С-приложений по исходному коду
