Интегрированная методика автоматизированного построения формальных поведенческих моделей C-приложений по исходному коду Юсупов Юрий Вадимович Специальность – Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Научный руководитель: проф. кафедры ИУС, ФТК Котляров Всеволод Павлович

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

3 Цели и задачи исследования Цель – разработка методики автоматизированного построения формальных поведенческих моделей C-приложений по исходному коду, пригодных для статического и визуального анализа поведенческих и структурных свойств. Задачи: анализ области автоматизированного построения формальных моделей по их исходному коду на основе сравнительного анализа промышленных инструментов возвратного проектирования и формальных нотаций; определение модели поведения для систем, реализованных на языке C, пригодной для статического и визульного анализа; создание методик формализации фрагментов исходного кода C-приложений с помощью выбранной формальной нотации; разработка программной реализации, позволяющей обеспечить генерацию формальных спецификаций по фрагментам исходного кода C-приложений; внедрение разработанной методики и программных средств в процесс производства и поддержки ПО.

4 Область исследования Возвратное проектирование – это процесс анализа системы с целью идентификации системных компонентов и их взаимодействий (поведенческих свойств) и создания представления системы в другой форме или на более высоком уровне абстракции. (E. Chikofsky, J. Cross) Цели возвратного проектирования: –создание альтернативных форм описания системы для облегчения понимания и повышения уровня осмысления; –восстановление утраченной информации о системе с целью восстановления документации; –построение моделей программ с целью верификации и тестирования. Методы возвратного проектирования: –Статический анализ. –Динамический анализ.

5 Инструментарий возвратного проектирования Целевая платформа Win32, Unix Win32, Unix Win32, Unix Win32, Unix Win32, Unix Win32 Поддержка языков C, C++, C#, Java C, C++, Java, Tcl, FORTRAN,COBOL C, C++ C, C++, JavaC, C++ Объем поддерж. кода (MLOC) >5>50.5 1

6 Сравнительный анализ формальных нотаций Критерии Теоретич. модель Инструмент. поддержки Текстовое предст-е Графич. предст-е Композ./ декомпоз. Мин. един. описания Поведенческ. сценарии MSCCSP Telelogic SDL TTCN, Telelogic TAU G2, VRS +--Сценарий- SDLCFSM Telelogic SDL TTCN +++ Кон.-авт. диаграмма + UMLCFSM Telelogic TAU G2 +++ Кон.-авт. диаграмма + Basic protocols ATSVRS+++ Базовый протокол + PromelaCSPSpin+--Процесс+ LotosCCS, CSPLOTOS+--Процесс- EstelleCNSMEDT+-- Кон.-авт. диаграмма + VDM-SLLPFVDM+--Функция- RSL VDM-SL, CSP RAISE+--Процесс-

7 Формализация Организация проекта из базовых протоколов Генерация поведенческих сценариев Старт Финиш Визуализация модели А А - Автоматический этап А А Р - Ручной этап Исходный код проекта (С) Формальная модель (Базовые протоколы) Поведенческие сценарии (MSC) Анализ кода и исправление найденных ошибок Р А Графические представления 7 Р VRS Klocwork Концепция предлагаемого подхода

8 Атрибутная транзиционная система – S – множество состояний; – А – множество действий; – T– множество размеченных переходов и неразмеченных (скрытых) переходов – L – множество атрибутных разметок; – – частично определенная функция разметки состояний. Аппарат описания модели поведения программной системы E = (e 1, e 2, e 3,…) M = (m 1, m 2, m 3,…) S in = (in 1, in 2, in 3,…) S out = (out 1, out 2, out 3,…)

9 Динамические аспекты модели поведения … int pid; int replyEvent; char *replyMessage; void *replyPointer; int len; int notification = 0; /* not notification by default */ char * rpcmode = ""; /*no extra text by default */ if (argc > 1 && strcmp (argv[1], "-listpm") == 0) { /* Get all postmaster! */ int bufferPid[100]; char* bufferText[100]; int noOfPM; int i; noOfPM = SPFindActivePostMasters (bufferPid, bufferText, 100); for (i = 0; i < noOfPM; i++) { if (bufferText[i] != NULL) { printf ("Pid: %d, Created: %s\n", bufferPid[i], bufferText[i]); SPFree (bufferText[i]); } /* break when ready*/ exit (0); } if ( argc > 3 && !strcmp( argv[argc-1], "-notification" ) ) { notification = 1; rpcmode = "NOTIFICATION"; argc--; argv[argc] = 0; /* hide this flag to avoid later confusion */ } if (argc < 3) { printf ("usage: %s [...] [- notification]\n", argv[0]); exit (1); … 1. Исходный код 3. Дерево поведения 4. Поведенческие сценарии 2. Базовые протоколы

10 Методика 1: сохранение потока управления программы … … st_2 st_3 st_4 st_5 st_3 st_4 st_5 st_6 bp 2 bp 4 bp 3 bp 5 FalseTrue for while do- while switch defaultcase1case2 … Фрагменты систем переходов для нелинейных фрагментов кода Связь базовых протоколов по состояниям агента-приложения st_2, st_3, st_4, st_5, st_6 – состояния агента-приложения; bp 2, bp 3, bp 4, bp 5 – базовые протоколы.

11 Методика 2: формализация вызовов функции (1) начало конец БП вызывающей функции 1 Протокол-коннектор для передачи управления в вызываемую функцию 2 Протокол-коннектор для возвращения управления в вызывающую функцию 4 БП вызывающей функции 5 РП вызываемой функции 3 1) bp n =(a n-1,a n ) 2) cp 1 =(a n,b 1 ) 3) ep=(b 1, b m ) 4) cp 2 =(b m,a n+1 ) 5) bp n+1 =(a n+1,a n+2 ) (a n-1, a n ) A (b 1, b m ) B (a n+1 ) A (b m ) B (a n ) A (b 1 ) B (a n+1, a n+2 ) A A – множество состояний вызывающей функции B – множество состояний вызываемой функции

12 Графическое представление шаблона MSC диаграммы mscdocument ; msc ; ENV#envir: instance; MODEL#model: instance; all: condition PRE /*MODEL(model, ); */; MODEL#model: action ' '; MODEL#model: out ( ) to ENV#env; ENV#env: in ( )from MODEL#model; all: condition POST /*MODEL(model, ); */; ENV#envir: endinstance; MODEL#model: endinstance; endmsc; Текстовое представление шаблона MSC диаграммы Методика 3: построение базовых протоколов

13 – функция_Det – базовые протоколы, описывающие поведение функции на детальном уровне – ф ункция_Comp – базовые протоколы, описывающие поведение функции на некотором уровне абстракции – !Connectors – протоколы-коннекторы для моделирования вызовов функций – EP_ функция – расширенные протоколы, описывающие поведение вызываемых функций Методика 4: структурирование базовых протоколов 1 директория 2 файл директория 3 файл директория функция 5 файл директория функция !Connectors функция_Det функция_Comp EP_функция 4 файл директория функция функция_Det функция_Comp

14 В рамках работы для решения поставленных задач и реализации разработанных методик создан следующий инструментарий: Программная поддержка c c c h h Формальная модель Динамически подключаемая библиотека Исходные файлы обработчика Приложение dll Исходные C-файлы Базовые протоколы Klocwork Объект разработки Конфигурационный файл dll АСД

15 Метрика оценки объема модели k – количество функций в проекте; BP – количество базовых протоколов, кодирующих детальное поведение функции; EP – количество расширенных протоколов, кодирующих поведение вызываемых функций; CP – количество протоколов-коннекторов, необходимых для моделирования вызовов функций. LOC – количество строк кода функции, каждая из которых содержит хотя бы один оператор; i, e, f, s, w, F – количество операторов if, else, for, switch, while и вызовов функций в коде функции соответственно.

16 Общая схема применения методики Исходный код (С) 1 Klocwork Insight Результаты анализа кода 3 Специальный обработчик Базовые протоколы 7 Исправление исходного кода Описание окружения Описание сигналов VRS Генерация трасс Построение диаграмм Изменение уровня абстракции 5 6 ТрассыДиаграммы Верификация 1616 Требования 1414 Структури- рованный проект из базовых протоколов 9 8 Критериальные цепочки 1515 Исправления Анализ результатов 1717 VRS

17 Пилотирование и применение разработанного комплекса методик и программных средств проведено в следующих 4 проектах: Учебный проект. Применение методики к исходному коду приложения с целью проверки всех разработанных методик и программных средств (40 BPs). Проект автомобильного радио (CarRadio). Применение методики структурирования базовых протоколов для получения проекта, структура которого позволяет работать с моделью покомпонентно и на разных уровнях абстракции (70 BPs). Проект анализатора A-деревьев. Применение методики к исходному коду реализованного обработчика с целью проверки корректности его реализации (8000 BPs). Приложение для тестирования мобильного телефона. Применение методики к исходному коду приложения для мобильного телефона с целью верификации реализованного приложения (70000 BPs). Проекты пилотирования и применения методики

18 Анализ результатов применения Зависимость трудозатрат от размеров модели (аппроксимация на основе пилотирования) чел.-часа Тип А Тип Б - трудозатраты автоматиз. подхода - трудозатраты ручного подхода - трудозатраты автоматиз. подхода - трудозатраты ручного подхода

19 Анализ результатов применения Зависимость размеров моделей от уровня абстракции (аппроксимация на основе пилотирования)

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

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

22 СПАСИБО ЗА ВНИМАНИЕ