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

Введение.

1. Обзор подходов проверки качества программного обеспечения.

1.1. Методы обеспечения качества программного обеспечения.

1.2. Методы и особенности тестирования.

1.2.1. Методы автоматизации тестирования.

1.2.2. Инструментарий тестирования.

1.3. Формальный подход к проблеме обеспечения качества ПО.

1.3.1. Математический аппарат моделей программ.

1.3.2. Обзор моделей программ.

1.4. Методы верификации.

1.4.1. Нотации описания систем.

1.4.2. Дедуктивные методы верификации.

1.4.3. Методы проверки на модели.

1.5. Инструментарий верификации.

1.5.1. Сравнительный анализ средств верификации. ф Выводы.

2. Методики интегрированной технологии верификации и тестирования.

2.1. Общая схема технологии автоматизированной верификации и тестирования.

2.2. Используемые формальные языки. щ 2.3. Основы метода базовых протоколов.

2.3.1. Базовые протоколы.

2.3.2. Язык базовых протоколов.

2.3.3. Базовый протокол в MSC.

2.4. Система верификации VRS.

2.5. Система автоматизации тестирования ТАТ.

2.6. Обзор методик интегрированной технологии верификации и тестирования.

2.6.1. Поиск ошибок в спецификациях.

2.7. Методика формализации требований на основе базовых протоколов (МВР).

2.7.1. Создание БИА.

2.7.2. Создание БИС.

2.7.3. Создание БИФ. ф 2.8. Методика доказательства заданных свойств системы на основе её модели на языке

SDL с последующей генерацией кода (SAC).

2.9. Методика генерации тестового набора (TG).

2.10. Методика доказательства детерминированности поведения системы (ТСС).

2.11. Методика проверки аннотированных сценариев поведения системы (АС).

2.12. Методи ка автоматизации тестирования (ТАТ).

Выводы.

3. Программная поддержка технологий автоматизации тестирования и верификации.

3.1. Программная поддержка интеграции подсистем верификации и тестирования.

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

3.2.1. Блок запуска генерации.

3.2.2. Блок анализа конфигурации.

3.2.3. Блок генерации.

3.3. Подсистема настройки на область тестирования.

3.3.1 Графический пользовательский интерфейс.

3.3.2 Генератор интерфейсного модуля.

• 3.4. Характеристика разработанных программных средств.

Выводы.

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

4.1. Состав экспериментального комплекса.

4.2. Применение технологии в телекоммуникационных проектах.

4.3. Применение технологии в проектах связанных с мобильной телефонией.

Ш 4.4. Применение технологии в проектах встроенных применений.

4.5. Учебные проекты.

4.6. Общая статистика и анализ результатов применения технологии.

4.7. Оценки применения технологии в больших промышленных проектах.

Выводы.

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

Для создания качественного ПО прежде всего необходимо обеспечить ясность в постановке задачи и методах её решения. Поэтому с ростом сложности ПО возрастает потребность в средствах визуального моделирования и проектирования, а также в специалистах, знающих и умеющих использовать их на практике. Программистское сообщество осознаёт, что резервы повышения производительности труда при создании качественного ПО связаны с системным подходом и использованием передовых методов и средств автоматизации разработки больших программных проектов. В данном направлении ведётся значительное количество исследований по созданию новых стандартов и инструментальных средств, которые объединяются в рамках такого направления как Computer Aided Software Engineering (CASE).

Стоимость исправления ошибок в пределах жизненного цикла продукта экспоненциально растёт в соответствии с фазой разработки [Воет]. Самой дешёвой фазой, на которой необходимо по возможности искоренить как можно больше ошибок является разработка требований и спецификаций.

Когда изменяются требования, основной проблемой становится корректировка тех частей продукта, которые уже прошли стадии кодирования и тестирования. Естественно, что подобные действия являются достаточно трудоёмкими, так как возвращают разработчиков на начальные этапы проекта в тот момент, когда код уже практически написан и ли тестируется. Подобного рода корректировки расходуют 30-50 % общего бюджета разработки [Воет], а ошибки в требованиях обходятся в 70-85% общей стоимости корректировки кода [Leffingwell].

120 100 80 60 40 20

I-1

О Series 1 требования разработка кодирование тестирование работа с продуктом

Рис. 1 Стоимость исправления ошибок в зависимости от стадии проекта

Как показывает рис. 1, гораздо сложнее исправить дефекты, которые найдены при эксплуатации продукта, чем в процессе его создания [Grady]. Следовательно, предотвращение ошибок в требованиях и обнаружение их на ранних этапах проекта сильно уменьшает объём корректировок продукта и таким образом сокращает общую стоимость разработки ПО. Именно поэтому в последнее время всё большее внимание специалистов в области разработки ПО уделяется различным стандартам позволяющим разрабатывать формальные требования на систему. Наиболее известными графическими стандартами являются UML [uml], SDL [sdl], MSC [msc]. Использование формального языка или процедуры для создания требований позволяет значительно сократить вероятность появления ошибки в спецификациях.

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

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

Существующие в настоящее время на рынке технологии и инструменты для разработки ПО далеко не во всем обеспечивают решение поставленной проблемы. Это является следствием их узкой направленности на определённые этапы жизненного цикла. Существуют эффективные нотации для описания требований, такие как: UML, MSC, SDL, VDM, Alloy, NP, В, RSL, LOTOS, ML, Isar, PVS, CASL, SMV, Promela, Esterel, SCR, Murphi и другие. Представленные нотации основаны на таких широко известных моделях программ как сети Петри (Петри), конечные автоматы (Мили, Мура и др.), темпоральные логики (Приора), алгебры параллельных процессов(Милнера, Хоара, Бергстры и Клоппа), традиционные системы(Парка), агенты и среды(Летичевского и Гилберта). В тоже время существует множество инструментов верификации, разработанных в различных научных лабораториях по всему миру: LOTOS (организация ISO), 8рт(лаборатория BellLabs), Кгопоз(лаборатория VERIMAG), 8СЯ(лаборатория NavalResearch), VRS (организация ISS) и другие, и инструменты автоматизации тестирования созданные известными компаниями по разработке ПО, это Rational Rose компании IBM, Telelogic TAU компании Telelogic AB, TAT компании Motorola, Together компании Borland и другие.

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

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

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

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

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

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

3. Проведён анализ инструментов верификации с целью выявления возможностей по их использованию в промышленном процессе создания ПО.

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

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

6. Разработан и программно реализован алгоритм преобразования модели, основанной на представлении свойств системы в виде базовых протоколов, в язык SDL.

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

8. Проверена работоспособность предложенной технологии и инструментальных средств в нескольких проектах по производству ПО.

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

Основные результаты работы докладывались и обсуждались на семинарах ЗАО «Моторола ЗАО» (Санкт-Петербург), Учебной лаборатории Моторолы в СПбГТУ, конференции IEEE Russia Northwest Section, 110 Anniversary of Radio Invention и конференции SABA (Science Advisory Board Associates) 2005.

По материалам диссертационной работы опубликовано 9 печатных работ.

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

Заключение

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

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

1. Проведён анализ существующих методов и средств автоматизации тестирования и верификации, существующих в настоящее время на рынке ПО.

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

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

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

5. Разработаны программные реализации, позволяющие объединять различные методики с целью повышения качества ПО.

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

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

Полученные в ходе работы основные результаты:

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

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

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

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

5. Разработана методика доказательства заданных свойств системы (SAC) на основе её модели на языке SDL. В рамках методики описаны особенности верификации моделей на языке SDL с использованием инструмента VRS и предложены подходы к автоматическому переходу на стадию тестирования.

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

7. Разработана методика доказательства детерминированности поведения системы (ТСС), позволяющая определять возможные места возникновения недетерминизмов.

8. Разработана методика проверки аннотированных сценариев поведения системы (АС), позволяющая проводить проверку полноты описания системы в виде множества базовых протоколов.

9. Разработана методика автоматизации тестирования (ТАТ), позволяющая использовать результаты верификации на стадии тестирования.

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

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

12. Доработана подсистема настройки на область тестирования, включённая в состав инструмента ТАТ.

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

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

В практическом плане на базе полученных научных результатов был разработан комплекс программных средств, предназначенных для совместного использования верификации и тестирования. Программный комплекс был использован в компании Motorola в 6 программных проектах по разработке встроенных систем в таких областях как: разработка мобильных устройств, телекоммуникационных и телематических систем. Кроме того, созданная технология и программные средства были внедрены в проекте разработки функциональной программной подсистемы управления узлами связи "83Т54-2М" в ОАО "Интелтех" и проекте "Исследование работы контроллера в системе распределённого электропитания железнодорожного вагона" в ЗАО "Северо-Западная лаборатория Лтд". Созданные методики и программные средства могут быть использованы для обеспечения качества реактивных систем в широком спектре встроенных применений.

Разработанные методы и средства технологии интегрированной верификации и тестирования программных изделий использованы в курсе лекций "Введение в технологии верификации" кафедры "Информационные и Управляющие Системы" СПбГТУ.

Общий объем разработанного программного обеспечения, вошедшего в программный комплекс поддержки интегрированной технологии, составил около 500 килобайт исходного кода на языках Tel и С++; объем документации на разработанное программное обеспечение -более 200 страниц.

1. Valmari, A., The State Explosion Problem, Lectures on Petri Nets 1. Basic

2. Models, Lecture Notes in Computer Science 1491, Springer (1998), 429(528.2. www.eiffel.com3. http://vl.fmnet.info/ формальные методы.

3. С. A. R. Hoare,"Communicating Sequential Processes", P-H 1985.5. http://www.cs.bell-labs.com/cm/cs/what/formalmethods/

4. G.J. Holzmann, "PAN: A Protocol Specification Analyzer," Technical Report TM81-11271-5, AT&T Bell Laboratories, Mar. 1981.

5. G.J. Holzmann, "Tracing Protocols," AT&T Technical J., vol. 64, pp. 2,413-2,434, Dec. 1985.

6. G.J. Holzmann, "An Improved Protocol Reachabily Analysis Technique," Software, Practice and Experience, vol. 18, no. 2, pp. 137-161,1. Feb. 1988.

7. M.Y. Vardi and P. Wolper, "An Automata-Theoretic Approach to

8. Automatic Program Verification," Proc. First IEEE Symp. Logic in

9. Computer Science, pp. 322-331, 1986.

10. Липаев B.B. «Тестирование программ» //М.:Радио и связь, 1986.

11. И. Непомпяпцций В.А., Рякин О.М. Прикладные методы верификации программ //М.:Радио и связь, 1988.

12. В.А. Захаров, Д.В. Царьков. Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL на модели и их применение для верификации параллельных программ. // Программирование, 1998, №4, с. 3-18

13. Jones90. С.В. Jones. Systematic Software Development Using VDM, 2/e,. Prentice Hall International Series in Computer Science, Hemel Hempstead, UK, 1990.

14. Abrial96. The B-Book: Assigning Programs to Meanings, J.-R. Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5. 850 pages

15. ESTELLE87. ISO Information Processing Systems - Open Systems Interconnection -"ESTELLE — A Formal Description Technique Based on an Extended State Transition Model", DIS 9074,1987.

16. Каг. Ю.Г. Карпов Теория алгоритмов и автоматов. Санкт-Петербург 1998.

17. Karl. Ю.Г. Карпов Верификация распределенных алгоритмов и протоколов, курс лекций.

18. SMV92. K.L.McMillan, The SMV system, Carnegie Mellon University, 1992

19. Holzmann91. Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991

20. Spivey88. J.M. Spivey. Understanding Z, A Specification Language and its Formal Semantics. Cambridge University Press, 1988.

21. Mil90. R. Milne. The semantic foundations of the RAISE specification language. RAISE Report REM/11, STC Technology Ltd, 1990.

22. Gordon93. M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL. Cambridge University Press, 1993.

23. Nipkow02. Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel, Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Springer, LNCS, v.2283, 2002.

24. K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993

25. G. M. Weinberg, The Psychology of Computer Programming. New York: Van Nostrand Reinhold, 1971.

26. G. M. Myers, "A Controlled Experiment in Program Testing and Code Walkthroughs/inspections", Commun. ACM, 21(9), 760-768(1978).

27. M. P. Perriens, "An Application of Formal inspections to Top-Down Structured Program Development", RADC-TR-77-212, IBM Federal Systems Div., Gaithersburg, Md., 1977 (NTIS AD/A-041645).

28. J.Burch, E.Clarke, D.Long, K.McMillan, and D.Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4), 1994.

29. Alur R. and Dill D.L. A theory of timed automata. Theoretical Computer Science, 126(2): 183 -- 235.

30. СП1. Котов В. E. Сети Петри. M.: Наука, 1984.

31. СП2. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984. СПЗ]. Jensen К. Coloured Petri nets: Basic concepts, analysis methods and practical use. -- Berlin a. o.: Springer-Verlag, 1996. ~ Vol. 1. Basic concepts.

32. СП4. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри /В.А. Непомнящий, А.В. Быстров и др. -- Новосибирск, 1998. — 140 с.

33. ACP. J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1): 109-137, 1984.

34. Abrial96. The B-Book: Assigning Programs to Meanings, J.-R. Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5. 850 pages

35. ЬЗ. http://www.bitd.clrc.ac.uk/Activity/ACTIVITY=BUT

36. Ь4. http://rodin.cs.ncl.ac.uk/

37. Ь5. https://gna.org/projects/brillant

38. Dij76. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976 Wir71] N. Wirth. Program Development by Stepwise Refinement. Communications of the ACM, (14):221 227,1971

39. Jon86. C.B. Jones. Systematic Software Development using VDM. Prentice-Hall Series in Computer Science. Prentice-Hall International, 1986

40. Mil90a. R. Milne. The proof theory for the RAISE specification language. RAISE Report REM/12, STC Technology Ltd, 1990.

41. Mil90. R. Milne. The semantic foundations of the RAISE specification language. RAISE Report REM/11, STC Technology Ltd, 1990.

42. BD92a. D. Bolignano and M. Debabi. On the Foundations of the RAISE Specification Language. LACOS Report Bull/DB/27, Bull Corporate Research Center, June 1992.

43. Carchiolo-Faro-Mirabella-Pappalardo-Scollo-1986. Vincenza Carchiolo, Alberto Faro, O. Mirabella, Giuseppe Pappalardo, and Giuseppe Scollo. A LOTOS specification of the PRO WAY highway service. IEEE Transactions on Computers, C-35(l l):949-968, 1986.

44. Clark-199lb. R. G. Clark. The development of concurrent ADA systems from LOTOS specifications. In R.J Mitchell and D. Simpson, editors, ADA into the 90's, pages 115-129. Woodhead Publishing Ltd, 1991.

45. Clark-1992a. R. G. Clark. LOTOS design-oriented specification in the object-based style. Technical Report CSM-84, Department of Computing Science and Mathematics, University of Stirling, FK9 4LA Stirling, Scotland, April 1992.

46. Purvis-1990. J. B. Purvis. The use of LOTOS for the specification of graphics software. Technical Report CSTR-90-5, Department of Computer Science, Brunei University, Middlesex, UK, July 1990.

47. Reade-1992. Christopher M. P. Reade. Process algebra in the specification of graphics standards. Technical Report CSTR-92-1, Department of Computer Science, Brunei University, Middlesex, UK, September 1992.

48. Microprocessing and Microprogramming, 38:589-596,1993.

49. Faci-Logrippo-1993a. Mohammed Faci and Luigi M. S. Logrippo. Specifying hardware in LOTOS. In Proc. Computer Hardware Description Languages and Their Applications XI, pages 305-312. North-Holland, Amsterdam, Netherlands, April 1993.

50. Thomas-1994a. MuffyH. Thomas. The story of the Therac-25 in LOTOS. High Integrity Systems Journal, 1(1):3-15, February 1994.

51. Trafford-1997. Paul Trafford. The Use of Formal Methods for Safety-Critical Systems. PhD thesis, School of Computer Science and Electronic Systems, Kingston University, Kingston-upon-Thames, UK, October 1997.

52. Proc. Protocol Specification, Testing and Verification XIII, pages 175-190. North-Holland, Amsterdam, Netherlands, May 1993.

53. SMV92. K.L.McMillan, The SMV system, Carnegie Mellon University, 1992cad. http://www.cadence.com/index.aspx

54. International Organization for Standardization-Information Processing Systems-Open Systems Interconnection. Lotos-A formal description technique based on the temporal ordering of observational behavior. ISO Standard 8807. Geneva, Sep. 1988.

55. TLA. L. Lamport. Introduction to TLA. SRC Technical Note 1994-001, 1994.

56. TLA1. L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 872-923, May 1994.

57. TL. A. Pnueli. The temporal logic of programs. In: Proc. of the 18th Annual Symposium on the Foundations of Computer Science, 46-52, Nov. 1977.

58. CTL*. E. Emerson. Temporal and modal logic. In: J. van Leeuwen editor: Handbook of Theoretical Computer Science, Elsevier, (B):997-1072.

59. ML.E. Emerson and J. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. of Сотр. and System Sci., 30(l):l-24,1985.

60. ML1. M.J. Fisher and R. E. Ladner. Propositional modal logic of programs. In Proc. 9th ACM Ann. Symposium on Theory of Computing, 286-294.es. http://www-cad.eecs.berkeley.edu/Respep/Research/hsc/abstract.html

61. Mu. "Better Verification through Symmetry," C. Norris Ip and David L. Dill, International Conference on Computer Hardware Description Languages, April 26-28, 1993, pp 87-100.

62. Mul. State Reduction Using Reversible Rules C. Norris Ip and David L. Dill, 33rd Design Automation Conference, June 1996.

63. Mu2. Verifying Systems with Replicated Components in Murphi C. Norris Ip and David L. Dill, International Conference on Computer-Aided Verification, 1996

64. Mu3. Improved probabilistic verification by hash compaction, Ulrich Stern and David L. Dill, Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working

65. Mu4. Parallelizing the Murphi Verifier, Ulrich Stern and David L. Dill, 9th International Conference on Computer Aided Verification, 1997

66. Mu5. Using Magnetic Disk instead of Main Memory in the Murphi Verifier, Ulrich Stern and David L. Dill, CAV '98.

67. POTS. CONSISTENCY OF THE TELECOMMUNICATION TASK POTS. A.A.Letichevsky, J.V.Kapitonova, V.A.Volkov, S.L.Krivoi, A.A.Letichevsky, jr. 12 September 2001

68. CM. UML Telelogic Tau G2 Technology Vsevolod Kotlyarov, Pavel Drobintsev

69. Rational. http://www-306.ibm.com/software/rational/

70. UniTesK. http://www.unitesk.com/

71. TVGS. http://www.t-vec.com/solutions/tvec.php

72. CTG. http://www.verifvsoft.com/en conformiq testgenerator.html

73. Reactis. http://www.reactive-svstems.com/

74. TestMaster. http://testmaster.sourceforge.net/

75. Rhapsody. http://www.ilogix.com/subIevel.aspx?id=218

76. РТК. http://motlabs-uk.baseng.comm.mot.com/proiects/ptk/ Together] http://www.borland.com/us/products/together/index.html