Интегрированная методика автоматизированного построения формальных поведенческих моделей С-приложений по исходному коду тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Юсупов, Юрий Вадимович

• Юсупов, Юрий Вадимович
• кандидат технических наук
• 2009

Оглавление диссертации кандидат технических наук Юсупов, Юрий Вадимович

ВВЕДЕНИЕ.

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

Список литературы диссертационного исследования кандидат технических наук Юсупов, Юрий Вадимович, 2009 год

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.