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

На правах рукогшси

[оЦ^

Юсупов Юрий Вадимович

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

Специальность 05.13.11 -Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат

диссертации на соискание ученой степени кандидата технических наук

Санкт - Петербург - 2009

003474465

Работа выполнена в Государственном образовательном учреждении высшего профессионального образования «Санкт-Петербургский государственный политехнический университет».

Научный руководитель - кандидат технических наук, профессор Котляров Всеволод Павлович

Официальные оппоненты - доктор технических наук, профессор

Воробьев Владимир Иванович - кандидат физико-математических наук, доцент Кознов Дмитрий Владимирович

Ведущая организация - Федеральное государственное унитарное предприятие «Научно-производственное объединение «Импульс»

Защита состоится « Ц » сеи 7Яс>~^>$ 2009 г. в часов на заседании диссертационного совета Д 212.229.18 при ГОУ ВПО «Санкт-Петербургский государственный политехнический университет» по адресу: 195251, Санкт-Петербург, Политехническая ул., д.29,9 уч. корп., ауд. 325.

С диссертацией можно ознакомиться в Фундаментальной библиотеке ГОУ ВПО «Санкт-Петербургский государственный политехнический университет».

Автореферат разослан « » СМ/О 1/и? 2009 г. Ученый секретарь

диссертационного совета

Васильев А.Е.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

- определения базового инструмента для реализации метода автоматизированного

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

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

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

- определения модели поведения приложений на основе выбранной формальной

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

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

помощью выбранной формальной нотации;

- разработки программных средств, обеспечивающих автоматизацию построения

формальных моделей С-приложений по исходному коду;

- проверки работоспособности предложенных методик и инструментальных средств в

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

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

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

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

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

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

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

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).

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

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

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

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

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

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

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

машинописного текста, содержит 124 рисунка, 19 таблиц, список литературы - 100 наименований.

СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

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

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

Во второй главе представлена концепция автоматизированного подхода к построению и верификации моделей поведения приложений, реализованных на языке С, с использованием принципов инсерционного программирования, разработанного A.A. Летичевским, в котором система, специфицируемая базовыми протоколами, представляется в виде взаимодействующих в среде агентов. Агенты и среды рассматриваются как объекты разных типов, обладающие поведением, представляемым с помощью атрибутных транзиционных систем, в которых помимо разметки переходов используется разметка состояний. Атрибутная традиционная система (<S,A,T,L,l>)~ это набор следующих компонентов: 5- множество состояний; А— множество действий; TcSxAxSvSxS- множество размеченных переходов (л—>.?') и неразмеченных (скрытых) переходов (s -> s'); L- множество атрибутных разметок; l:S-» £ - частично определенная функция разметки состояний.

В свою очередь, базовый протокол описывает переход транзиционной системы и определяется тройкой а -»< Р > ß, где а vi ß - пред- и постусловие соответственно, а Р -процесс базового протокола. Условия а и ß представляются с помощью логических выражений некоторого базового языка и определяют условия на множестве состояний системы. На рис. 1 представлен базовый протокол в графической нотации, на котором отмечены три его составляющих: 1 - предусловие, 2 - процессная часть, 3 - постусловие.

Последовательность базовых протоколов (трасса) определяет историю функционирования системы, характеризующую ее поведение: .т0————Ьрг —, где л'о, 5| - состояния модели; Ьр\, Ьрг - базовые протоколы.

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

Состояния £ (агент-окружение) и М (агент-приложение) определены как некоторые глобальные состояния. Каждое глобальное состояние содержит в себе множество простых состояний (Е = {е|, в2,...} и М = {ттг,...}), между которыми осуществляются внутренние переходы. Набор сигналов 5/я№„= {-?,ль определяет множество входных сигналов

для агента-приложения (М), а 30и, (5„„, (5„„,|, л„„,2,...}) - выходных.

Простые состояния агента-приложения соответствуют состояниям вычисления программы, определяемым парами (состояние управления, состояние данных). Состояние управления - это очередность (порядок) операторов исходной программы, а состояние данных - соответствие между переменными и их значениями. Переход между простыми состояниями агента-приложения определяется следующим образом: если в точке Р\ программы Я выполняется оператор ор, преобразующий данные из состояния й\ в состояние Д2 и передающий управление в точку Р2, то в модели имеется переход (Р\, й\)-¥(Рь £>г). Такой переход кодируется базовым протоколом, предусловие которого содержит описание состояния агента-приложения до выполнения оператора, а постусловие - описание состояния после выполнения. Процессная часть базового протокола включает в себя описание действия и сигнал взаимодействия между агентом-приложением и агентом-окружением, которые служат для наблюдения за изменениями в поведении модели программы. Эти изменения характеризуются такими действиями как вызовы функций, а также использование и изменение переменных при выполнении различных операций над ними.

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

Рис. 2. Обобщенное представление модели системы

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

Технологическая цепочка разработанной концепции представлена на рис. 3.

Рис. 3. Технологическая цепочка применения разработанного подхода

Данную цепочку можно условно разбить на 4 этапа.

Этап I. Первый этап заключается в проверке исходного кода (1) с целью исправления найденных в нем ошибок и дефектов на основе полученных результатов анализа (3). Анализ кода проводится с помощью встроенных обработчиков статического анализатора Klocwork Insight (2). На данном этапе осуществляется следующее преобразование: (SC) (SCcorr), где SC- исходный код; SCcorr - свободный от ошибок исходный код.

Этап II. Второй этап связан с автоматическим построением по свободному от ошибок коду приложения (1) формальной модели (5) в виде структурированного множества базовых протоколов с помощью реализованного в настоящей работе обработчика (4). На данном этапе осуществляется следующее преобразование: (SCcorr) (Ж«-), где SCcorr - свободный от ошибок исходный код; Msc = Фр\, Ьрг,-.-) - формальная модель системы, определяемая структурированным множеством базовых протоколов.

Этап III. На третьем этапе с помощью системы VRS осуществляется построение (6, 8) поведенческих сценариев (трасс) (9), отражающих изменения в поведении модели (компонента), и графических диаграмм (7), отражающих поведенческие и структурные свойства модели (компонента). На данном этапе осуществляется следующее преобразование: (Msc,DET) (77?, GR), где DET = (det\, deti,...) - уровни абстракции, TR = (tr\, tn,...) - множество трасс, полученных в ходе моделирования поведения системы (компонента); GR = (gr\, gri,...) - множество графических диаграмм.

Этап IV. Четвертый этап - анализ и использование полученных на предыдущем этапе данных (10). Поведенческие сценарии применяются в процессе автоматизированной верификации, а графические диаграммы - в процессе документирования анализируемой системы. На данном этапе осуществляется следующее преобразование: (TR, GR) {DOC, VER), где DOC = (doc\, doci,...) - множество документов (12); VER = (ver¡, veri,...) -множество верификационных вердиктов (11).

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

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

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

где st_2, st_3, st_4, st_5 и st_6 - состояния агента-приложения, a bpi, Ьръ, bpi, bps - базовые протоколы, которые описывают переходы между этими состояниями, формализуя некоторую последовательность выражений программы с сохранением порядка их выполнения.

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

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

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

* Ь/>1 . . юпп, г . -о ЕР /' , се сот? т ....т _ 4--—>т/ --—у / _ г.ъ-=■—>_/ _ гг.--—> рл- >»;_6.„,

где т_Ьр$ и т_Ьрь базовые протоколы функции т\ ант, и С0ПП2 протоколы-коннекторы; ЕРJ расширенный протокол функции/. При этом, вместо расширенного протокола может использоваться сценарий из базовых протоколов, специфицирующий летальное повеление функции /I / ГЗ— ^ — "—>/ РЕ, где /_Ьр\,..,,)_Ьр„ базовые протоколы функции/

На рис, 5 продемонстрирован пример использования протоколов-коннекторов (С0ПП| и еопПт) на диаграмме взаимодействия двуч функций (т и Л представленных в виде композитных состояний (т и Эти состояния могут быть декомпозированы до внутренних графов переходов, отображающих детальное повеление функций.

m f

conn-ï

Рис. 5. Диаграмма взаимодействия двух функций

3, Методика построения базовых протоколов использует шаблон MSC.fR диаграммы (Рис. 6) и обеспечивает формирование составных частей для каждого базового протокола.

mscdacuinent <иыя файла>; msc <-'"■ оаэового протокола>; ËHV#envii: instance; MODEL#mo de1 : instance ;

all: condition PRE /*MODEL [model, ¿состояние агента-г1риложения>) ,■ <атрибуты и параметры агента-приложения^/; MODELttmodel: action *<действие>';

MODEUmodel : out <сигнал>(¿параметра сигнала>) to ËNVtenv;

EMV#envir; in <сигнал> (-¡параметры сигнала?-) from MODELA mode 1 ;

all: condition POST /»MODEL(model, ¿состояние агента-приложения:») ;

¿атрибуты и параметры агента-приложения>*/;

ENV#envir: endinstance ;

MODEUmodel : endins tance :

endmsс ;

Put. 6. Шяолои MSC.'PR диаграммы

Используемые в шаблоне данные:

- model, envir - агент-приложение и агент-окружение;

- MODEL, ENV - типы агентов model и envir;

- MODEL#model, ENV#envir - процессы (сущности), отображающие агент-приложение

и агент-окружение на MSC диаграмме.

Методика осуществляет следующее преобразование:

(Node, TEMPI) TEMPL (F, D, PRE, AC, SI, POST), где Node - выражение кода, TEMPL - шаблон MSC/PR диаграммы, F - имя файла, D- имя базового протокола, PRE - предусловие, АС- действие, SI - сигнал, POST - постусловие.

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

директория

>

директория

• —| файл |

pii

директория

файл

функция

директория

файл

9

директория

функция

файл

функция Dct

функция Comp

функцияI

функция^

функцияСотр

¡Connectors

-- ЕРфункция

Рис. 7. Этапы методики структурирования базовых протоколов

На рис. 7 представлены основные этапы методики структурирования. На первом этапе в целевом проекте осуществляется построение иерархии директорий, соответствующей структуре исходного проекта (dir), в которых впоследствии создаются разделы (FI), соответствующие исходным файлам (/?). В этих разделах создаются директории (FU), соответствующие функциям файла, в которых в свою очередь осуществляется построение директорий для протоколов, специфицирующих детальное поведение функции (DET) и описывающих поведение на некотором уровне абстракции (COMP). Также здесь создаются разделы для расширенных протоколов (ЕР) и протоколов-коннекторов (CONN), необходимых для моделирования вызовов функций. Формально методика структурирования (STR) базовых протоколов может быть записана в виде: STR: (dir, ft) (dir, FI, FU, DET, COMP, EP, CONN).

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

разработанных методик подтверждена при их реализации и пилотировании в реальных программных проектах.

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

Обобщенная схема применения разработанного подхода приведена на рис. 8.

"3"

Исправление исходного кода

Рис. 8. Обобщенная схема применения разработанного подхода Вначале исходный код приложения (1) анализируется на наличие в нем ошибок и дефектов с помощью стандартных обработчиков (2) системы Klocwork Insight, использующей для анализа промежуточное представление кода в виде абстрактного синтаксического дерева (А-дерево). Результаты анализа выдаются в виде отчетов (3) и используются в процессе исправления ошибок.

Далее программный код в формате А-деревьев поступает на вход специального обработчика (4), осуществляющего построение, генерацию и структурирование базовых протоколов (8) и двух конфигурационных файлов, описывающих используемые данные (агенты, атрибуты) (5) и используемые в базовых протоколах сигналы (6). С помощью системы VRSClient полученные файлы организуются в структурированный проект (8), образующий формальную модель поведения программы. Работа с моделью осуществляется путем выделения множества базовых протоколов, характеризующих поведение одного или нескольких компонентов на некотором уровне абстракции (9), и последующего

построения (12) графических диаграмм (13) или запуска трассового генератора (10) для получения множества трасс (11).

На следующем этапе по исходным требованиям (14) формируются критериальные цепочки (15)- последовательности событий или состояний модели. Покрытие требования определяется нахождением трассы, содержащей соответствующую цепочку. Процесс поиска и выбора минимального набора трасс, обеспечивающего полное покрытие всех требований, поддерживается системой УЯБ в автоматическом режиме (16). На основе анализа результатов (17) верификации проводится дальнейшее исправление исходного кода(1), требований (14) или базовых протоколов (7).

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

- Тип А. Эти модели используются для анализа сразу после построения. Трудоемкость получения таких моделей с помощью автоматизированного подхода оценивается в 0,1 человеко-часа. Трудоемкость ручного построения моделей с типом А оценивается в 0,16*(кол-во протоколов) человеко-часов.

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

Для оценки размера модели (М) предложена формула, отражающая количество протоколов, которые будут получены по исходному коду системы с использованием разработанных средств и методик:

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

Количество базовых протоколов (BP) определяется по следующей формуле: BP = (LOC + \) + i + е +f + s + 2*w + F, где LOC- количество строк кода функции, каждая из которых содержит хотя бы один оператор; i, е,/, s, w, F - количество операторов if, else, for, switch, while и вызовов функций в коде функции соответственно.

к

(О

/=1

Количество расширенных протоколов (ЕР) и протоколов-коннекторов (СР) для функции определяется с помощью следующих формул: + и СР = 2*

где ^ и р""11^ - количество вызываемых функций, определенных и не определенных в проекте соответственно.

На основе экспериментальных данных, полученных в ходе пилотирования разработанного подхода, была установлена зависимость трудозатрат на построение моделей с типами А и Б от их размеров (Рис. 9).

Рис. 9. Трудоемкость ручного и автоматизированного подхода построения моделей

с типами Л и Б

Для моделей с типом А (Рис. 9, А) трудоемкость автоматизированного построения оценивается в 0,1 человеко-часа и не зависит от их размеров, тогда как трудоемкость ручного подхода формализации пропорционально растет с ростом количества базовых протоколов в модели. Для моделей с типом Б (Рис. 9, Б) наблюдается увеличение трудоемкости формализации автоматизированного подхода по сравнению с соответствующей оценкой для моделей с типом А (Рис. 9, А), что связано с ручными трудозатратами на внесение в базовые протоколы, полученные автоматически, дополнительной информации, уточняющей модель.

На основе результатов, представленных на рис. 9, была получена оценка выигрыша в трудоемкости автоматизированного подхода построения моделей с типами А и Б перед ручным. В первом случае (Рис. 9, А) выигрыш составляет несколько порядков даже при малых размерах моделей и растет с ростом их объемов. Во втором случае (Рис. 9, Б) преимущество автоматизированного подхода является трехкратным.

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

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

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

ЗАКЛЮЧЕНИЕ

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

Основными результатами диссертационной работы являются:

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

2. Методика спецификации фрагментов исходного С-кода приложений базовыми протоколами, отражающими изменения в поведении программы.

3. Комплекс методик, обеспечивающих:

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

исходной программы;

- спецификацию вызовов функций с использованием расширенных протоколов и

протоколов-коннекторов;

- построение и генерацию базовых протоколов с использованием шаблона MSC/PR

диаграммы;

- структурирование базовых протоколов с целью организации разработанной

структуры модели.

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

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

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

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Юсупов Ю.В., Котляров В.П. Автоматизация построения формальных поведенческих

моделей из программного кода // Научно-технические ведомости СПбГПУ. № 4 (63).

СПб.: Изд-во Политехнического ун-та. - 2008. - С. 146-153. (издание из перечня ВАК)

2. Юсупов Ю.В., Котляров В.П. Автоматическое построение верификационных моделей для приложений на языке С//Системное программирование. Вып. 3. СПб.: Изд-во С.-Петербургского ун-та. - 2008. - С. 97-108.

3. Юсупов Ю.В., Котляров В.П. Методы реинженерии формальных спецификаций поведенческих моделей // Вычислительные, измерительные и управляющие системы. Сборник научных трудов. СПб.: Изд-во Политехнического ун-та. - 2007. - С. 110-119.

4. Никифоров И.В., Юсупов Ю.В. Методика структурирования результатов возвратного проектирования С-программ для построения спектра моделей приложений // XXXVII Неделя науки СПбГПУ. Материалы межвузовской научно-технической конференции. 2428 ноября 2008 г. СПб.: Изд-во Политехнического ун-та. - 2008. - С. 88-89.

5. Никифоров И.В., Юсупов Ю.В. Получение сценариев поведения моделей системы с помощью интеграции трасс ее компонент//Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 17-18 марта 2009 г. СПб.: Изд-во Политехнического ун-та. - 2009. - С. 108-109.

6. Юсупов Ю.В., Дробинцев П.Д., Котляров В.П. Автоматизированный метод построения формальных моделей С-программ с помощью базовых протоколов // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 11-12 марта 2008 г. СПб.: Изд-во Политехнического ун-та. - 2008. - С. 95-96.

7. Юсупов Ю.В., Кирсанова O.A., Котляров В.П. Технология обратного проектирования для формализации исходного кода и построения модели программ // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 11-12 марта 2008 г. СПб.: Изд-во Политехнического ун-та. - 2008. - С. 97-99.

8. Юсупов Ю.В., Котляров В.П. Построение формальной модели программы с использованием "KLOCWORK INSIGHT ARCHITECT" // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 13-14 марта 2007 г. СПб.: Изд-во Политехнического ун-та. - 2007. - С. 77-78.

9. Yusupov Yu., Kotlyarov V. Automated Creation of Verification Model for C-programs // Second Spring Young Researchers' Colloquium on Software Engineering. Proceedings. Vol. 2. SPb., 2008.-P. 7-10.

Лицензия ЛР № 020593 от 07.08.97

Подписано в печать 04.06.2009. Формат 60x84/16. Усл. печ. л. 1,25. Уч.-изд. л. 1,25. Тираж 100. Заказ 4529Ь.

Отпечатано с готового оригинал-макета, предоставленного автором, в типографии Издательства Политехнического университета. 195251, Санкт-Петербург, Политехническая ул., 29.

ВВЕДЕНИЕ.

1 АНАЛИЗ МЕТОДОВ И СРЕДСТВ ПОСТРОЕНИЯ ФОРМАЛЬНЫХ МОДЕЛЕЙ ПО ПРОГРАММНОМУ КОДУ.

1.1 Возвратное проектирование.

1.2 Анализ промышленных инструментальных систем возвратного проектирования.

1.3 Анализ формальных нотаций, используемых в промышленности.

1.4 Выводы.

2 ИНТЕГРИРОВАННАЯ МЕТОДИКА СОЗДАНИЯ ПОВЕДЕНЧЕСКИХ МОДЕЛЕЙ С-ПРИЛОЖЕНИЙ ПО ИСХОДНОМУ КОДУ.

2.1 Концептуальная схема.

2.2 Технологическая цепочка и сценарий ее использования.

2.3 формальное представление программной системы.

2.4 Автоматическое преобразование исходного кода в формальные спецификации.

2.5 Создание модели поведения в виде сценариев из базовых протоколов.

2.6 Визуализация моделей программ из базовых протоколов.

2.7 Выводы.

3 РЕАЛИЗАЦИЯ МЕТОДИК ПОСТРОЕНИЯ ФОРМАЛЬНЫХ МОДЕЛЕЙ ПО ПРОГРАММНОМУ С-КОДУ.

3.1 Методика сохранения потока управления программы.

3.2 Методика формализации вызовов функций.

3.3 Методика построения базовых протоколов.

3.4 Методика структурирования базовых протоколов.

3.5 Выводы.

4 РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ МЕТОДИКИ ПОСТРОЕНИЯ ФОРМАЛЬНЫХ МОДЕЛЕЙ С-ПРИЛОЖЕНИЙ ПО ПРОГРАММНОМУ КОДУ.

4.1 Обобщенная схема применения интегрированной методики.

4.2 Применение интегрированной методики в учебном проекте.

4.3 Применение методики структурирования базовых протоколов в проекте CarRadio.

4.4 Применение интегрированной методики в проекте анализатора А-деревьев.

4.5 Применение интегрированной методики в промышленном проекте.

4.6 Al 1ализ результатов применения методики.

4.7 выводы.

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

Эффективность решения задач этих этапов (верификация, восстановление документации и пр.) обеспечивается путем восстановления модели реализованной программной системы из исходного кода (возвратное проектирование, 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) Для подтверждения работоспособности предложенные методики и разработанный инструментарий программной поддержки применены в реальных программных проектах. Анализ результатов показал эффективность применения разработанной методики автоматизированного построения формальных поведенческих моделей.

1. Автоматизированный реинжиниринг программ. Сборник статей / под ред. А.Н.Терехова и А.А.Терехова. СПб.: СПбГУ, 2000.

2. Ахтырченко К.В., Сорокваша Т.П. Методы и технологии реинжиниринга ИС. М., 2003. (Труды Института системного программирования РАН).

3. Баранов С.Н., Дробинцев П.Д., Летичевский А.А., Котляров В.П. Верификационная технология базовых протоколов для разработки и проектирования программного обеспечения // Программные продукты и системы. 2005. № 1(69). С. 25-28. ISSN-0236-235X.

4. Бурдонов И.Б., Демаков А.В., Косачев А.С., Максимов А.В., Петренко А.К. Формальные спецификации в технологиях обратной инженерии и верификации программы // Труды Института системного программирования РАН. М., 1999. № 1. С. 35-47.

5. Бурдонов И.Б., Косачев А.С., Пономаренко В.Н., Шнитман В.З. Обзор подходов к верификации распределенных систем. М., 2003. Труды Института системного программирования РАН.

6. Волкова Е.Д., Страбыкин А.Д. Методы композиции и декомпозиции исполняемых UML моделей. М., 2007. Труды Института системного программирования РАН.

7. Голубев А.А. Методики создания и внедрения агентов в прикладное и системное программное обеспечение для автоматизации тестирования и мониторинга встроенных вычислительных систем. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ. 2007. 150 с.

8. Дробинцев П.Д. Интегрированная технология обеспечения качества программных продуктов с помощью верификации и тестирования. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2006. 238 с.

9. Карпов Ю.Г. Теория автоматов и алгоритмов. Учебное пособие. СПб., 2000. 149 с.

10. Карпов А.Н. Технология настраиваемой генерации тестов по формальным спецификациям для встроенных приложений и программных интерфейсов, реализованных на Java-подобных языках. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2007. 145 с.

11. Касьянов В.Н., Евстигнеев В.А. Графы в программировании: обработка, визуализация и применении. СПб.: БХВ — Петербург, 2003.

12. Кознов Д.В. Визуальное моделирование компонентного программного обеспечения. Диссерт. на соискание уч. ст. канд. физ.-мат. наук. СПб.: СПбГУ. 2000. 82 с.

13. Котов В. Е. Сети Петри. М.: Наука, 1984. 160 с.

14. Летичевский А.А. Об одном классе базовых протоколов // Проблемы программирования. 2005. № 4. С. 3-19.

15. Летичевский А.А., Капитонова Ю.В., Волков В.А., и др. Спецификация систем с помощью базовых протоколов // Кибернетика и Системный Анализ. 2005. №4. С. 3-21.

16. Летичевский А.А. Верификация и тестирование интерактивных систем, специфицированных базовыми протоколами. Диссерт. на соискание уч. ст. канд. физ.-мат. наук. Киев, 2005. 138 с.

17. Летичевский А.А., Капитонова Ю.В., Летичевский А.А. (мл.) и др. Инсерционное программирование // Кибернетика и системный анализ. 2003. № 1. С. 19-32.

18. Питерсон Д. Теория сетей Петри и моделирование систем. М.: Мир, 1984. 264 с.

19. Применение методов теории реактивных систем в задачах моделирования и качественного анализа непрерывно-дискретных систем // http://home.imm.uran.ru/dolly/voll/parijs2/nodel0.html

20. Терехов А.А. Языковые преобразования в задачах реинжиниринга программного обеспечения. Диссерт. на соискание уч. ст. канд.физ.-мат. наук. СПб.: СПбГУ, 2002. 127 с.

21. Терехов А.А., Верхуф К. Проблемы языковых преобразований // Открытые системы. 2001. № 5-6. С. 54-62.

22. Юсупов Ю.В., Котляров В.П. Методы реинженерии формальных спецификаций поведенческих моделей // Вычислительные, измерительные и управляющие системы. Сборник научных трудов. СПб.: СПбГПУ, 2007. С. 110119.

23. Юсупов Ю.В., Котляров В.П. Автоматическое построение верификационных моделей для приложений на языке С // Системное программирование. Вып. 3. СПб.: СПбГУ, 2008. С. 97-108.

24. Юсупов Ю.В., Котляров В.П. Автоматизация построения формальных поведенческих моделей из программного кода // Научно-технические ведомости СПбГПУ. СПб., 2008. № 4 (63). С. 146-153. ISSN 1994-2354.

25. Alur R., Dill D.L. A Theory of Timed Automata // Theoretical Computer Science. 1994. № 126 (2). P. 183-235.

26. Arnold R.S. Software Reengineering. Los Alamitos: IEEE Computer Society Press, 1993.

27. ASMs // http://www.eecs.umich.edu/gasm/

28. Ball T. The Use of Control-Flow and Control Dependence in Software Tools. PhD thesis. University of Wisconsin-Madison, 1993.

29. Bergey J., Hefley W., Lamia W., Smith D. Reengineering Process Framework. Pittsburgh: Software Engineering Institute, Carnegie Mellon University, 1995.

30. Betty H.C. Cheng and Gerald C. Gannod, Abstraction of Formal Specifications from Program Code // Proceedings of the 3rd Annual International Conference on Tools with Artificial Intelligence, November 1990. P. 125-128.

31. Biggerstaff T. Design Recovery for Maintenance and Reuse // IEEE Computer. 1989. July. Pages 36-49.

32. Carriere S.J., Woods S., Kazman R. Software Architectural Transformation. Pittsburgh: Software Engineering Institute, Carnegie Mellon University, 1999.

33. CC-Rider // http://www.cc-rider.com/

34. Chikofsky E.J., Cross J.H. Reverse Engineering and Design Recovery: A Taxonomy // IEEE Software. 1990. № 7. P. 13-17.

35. CodeSurfer // http://www.grammatech.com/products/codesurfer/overview.html

36. Crystal FLOW // http://www.sgvsarc.com/productcrystalflow.htm

37. Drobintsev P., Kotlyarov V., Karpov A., Yusupov Yu. Usage of CASE Approach for Guaranteeing of Software Quality // Second Spring Young Researchers' Colloquium on Software Engineering. Proceedings. Volume 1. SPb., 2008. P. 7-11.

38. EDT // http://www-lor.int-evry.fr/edt/#INTRODUCTION

39. Eilenberg S. Automata Machines and Languages. Vol. A. New York: Academic Press, 1974.

40. Ernst M.D. Static and Dynamic Analysis: Synergy and Duality // In ICSE Workshop on Dynamic Analysis (WODA). Portland, Oregon, 2003. P. 24-27.

41. Ferrante J., Ottenstein K., Warren J. The Program Dependence Graph and its Use in Optimization // ACM Transactions on Programming Languages and Systems. 1987. № 9 (3), July. P. 319-349.

42. Gerald C.G., Betty H.C. Using Informal and Formal Methods for the Reverse Engineering of С Programs // In Proceedings of the 1996 International Conference on Software Maintenance // IEEE. 1996. P. 265-274.

43. Gerald C., Betty H.C., A Formal Approach for Reverse Engineering: A Case Study. In Proceedings of the 6th Working Conference on Reverse Engineering. 1999. October. P. 100-111.

44. German A. Software Static Code Analysis Lessons Learnt, on CS551/CS651 Safety-Critical Computing, Andy German, QinetiQ Ltd.

45. Hind M., Pioli A. Which Pointer Analysis Should I Use? In ACM SIGSOFT International Symposium on Software Testing and Analysis, 2000. P. 113-123.

46. Hoare C.A.R. Communicating Sequential Processes. P-H, 1985.

47. Holcombe M. X-machines as a Basis for Dynamic System Specification // Software Engineering Journal. 1988. Vol.8. №. 3. P. 69-77.

48. Horwitz S., Reps T. The Use of Program Dependence Graphs in Software Engineering // Proceedings of the Fourteenth International Conference on Software Engineering. New York: ACM, 1992. P. 392-411.

49. Horwitz S., Reps Т., Binkley D. Interprocedural Slicing Using Dependence Graphs // Proceedings of the ACM SIGPLAN 88 Conference on Programming Language Design and Implementation (Atlanta, GA, June 22-24, 1988). New York: ACM, 1988. July. P. 35-46.

50. Horwitz S., Prins J., Reps T. Integrating Non-Interfering Versions of Programs // ACM Transactions on Programming Languages and Systems. New York: ACM, 1989. № 11. P. 345-387.

51. ITU Recommendation Z.120: Message Sequence Charts. 11/1999.

52. IEEE Computer Society TCSE, 1990 // http://tcse.org/

53. IEEE Standard Glossary of Software Engineering Terminology IEEE Std 610.12-1990.

54. Imagix 4D // http://www.imagix.com/

55. Insight // http://sourceware.org/insight/

56. ITU Recommendation Z.100: Specification and Description Language. 08/2002.

57. JavaPathFinder // http://javapathfinder.sourceforge.net/

58. Klaus Havelund and Willem Visser, Program Model Checking as a New Trend // International Journal on Software Tools for Technology Transfer (STTT). 2002. Vol. 4. № 1 (October). P. 8-20.

59. Klocwork Extensibility Interface User's Guide, Document version 1.3. Klocwork, 2006.

60. Klocwork Insight // http://www.klocwork.com/products/insight.asp

61. Letichevsky A.A., Kapitonova Y.V., Volkov V.A., Vyshemirsky V.V., Letichevsky. A.A. (Jr.). Insertion Programming // Cybernetics and System Analysis. Kiev, 2003. № l.P. 16-26.

62. Letichevsky A.A., Kapitonova J.K., Letichevsky A.A. (Jr.). Insertion Programming and System Simulation // Proceedings XXVI International Workshop on Modeling of Developing Systems. Kiev, 2003. P. 19-20.

63. Letichevsky A.A. and Gilbert D.R. Agents and environments. In 1st International scientific and practical conference on programming, Proceedings 2-4 September, 1998. Kiev: Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine, 1998.

64. Letichevsky A., Gilbert D., A Model for Interaction of Agents and Environments // Resent Trends in Algebraic Development Techniques / In D. Bert, C. Choppy, P. Moses (Eds.). LNCS 1827. 1999. P. 311-328.

65. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. New York: Springer-Verlag, 1992.

66. Marca D.A., McGowan C.L. SADT Structured Analysis and Design Technique. McGraw-Hill, 1988. 437 p.

67. Muchnick S. Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, 1997. 880 p.

68. Milne R. The Proof Theory for the RAISE specification language. RAISE Report REM/12, STC Technology Ltd, 1990.

69. Milner R. Communication and Concurrency. Prentice Hall, 1989.

70. OMG Unified modeling language spesification (draft). Version 1.3R. http://www.rational.com/uml. 1999.

71. Park D.M.R. Concurrency and Automata on Infinite Sequences. In Proceedings 5th GI Conference. Vol. 104 of Lecture Notes in Computer Science. Springer-Verlag, 1981. P. 167-183.

72. Promela // http://spinroot.com/spin/Man/Quick.html

73. RAISE // http://www.iist.unu.edU/newrh/III/3/l/page.html

74. Reps Т., Horwitz S., Sagiv M., Rosay G. Speeding up Slicing. In SIGSOFT'94: Proceedings of the Second ACM SIGSOFT Symposium on the Foundations of

75. Software Engineering (New Orleans, LA, December 7-9, 1994); ACM SIGSOFT Software Engineering Notes 19, 5 (December 1994). P. 11-20.

76. Sommerville I., Software Engineering. 6th Edition. Addison-Wesley Publishing, 2002. 624 p.

77. Source-Navigator // http://sourcenav.sourceforge.net/

78. Spin // http://spinroot.com

79. Stephen Jo. Lint, а С program Checker // Computer Science Technical Report 65. Bell Laboratories, 1977, December. P. 72-81.

80. Sugiyama K., Tagawa S., Toda M. Methods for Visual Understanding of Hierarchical System Structures // IEEE Trans, on Systems, Man and Cybernetics. 1981. № 11(2). P. 109-125.

81. Telelogic TTCN Suite // http://www.telelogic.com/products/ttcn/index.cftn

82. Telelogic TAU G2 // http://www.telelogic.com/products/tau/tau/index.cfrn

83. Thomas W. Automata on Infinite Objects // Handbook of Theoretical Computer Science / J. van Leeuwen (ed.). Vol. B. Elsevier, 1990. P. 131-191.

84. Tip F. A Survey of Program Slicing Techniques // Journal of Programming Languages. 1995. № 3(3), September. P. 121-189.

85. VDM-SL //http://www.csr.ncl.ac.uk/vdm/bnf.html

86. VDM // http://www.vienna.cc/e/evdm.htm98. www.iprinet.kiev.ua/gf/naupp 1 .htm

87. Wong K., Tilley S., Muller H., Storey M.-A. Structural Redocumentation // IEEE Software. 1995. № 12(1), January. P. 46-54.

88. Yusupov Yu., Kotlyarov V. Automated Creation of Verification Model for C-programs // Second Spring Young Researchers' Colloquium on Software Engineering. Proceedings. Vol. 2. SPb., 2008. P. 7-10.