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

• Корчагин, Александр Сергеевич
• кандидат технических наук
• 2009

Оглавление диссертации кандидат технических наук Корчагин, Александр Сергеевич

Введение

Содержание

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

1.1. Анализ подходов к автоматизации проектирования информационных систем с помощью операторного моделирования.

1.2. Технология проектирования с явным выделением состояний

1.3. Анализ состояния и перспектив применения нормированных операторных отображений для решения задач верификации при анализе и синтезе проектных процедур.

1.4. Постановка задач исследования.

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

2.1. Пошаговая детализация операторных отображений низкоуровневых спецификаций.

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

2.3. Обратные операторные модели.

2.4. Выводы.

3. Элементы математического и лингвистического обеспечения корректирующих проектных решений.

3.1. Проектный этап реализации процедур анализа и синтеза средств верификации.

3.2. Методология и алгоритмизация описания и построения корректирующих проектных решений.

3.3. Лингвистическое обеспечение процессов анализа и синтеза проектных процедур.

3.4. Лингвистическое обеспечение межинтсрфейсного взаимодействия.

3.5. Выводы.

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

4.1. Особенности реализации алгоритмов анализа и синтеза.

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

4.3. Особенности разработки и верификации информационной системы управления научным журналом.

4.4. Проектирование программной системы идентификации характеристик неоднородных систем с интеграцией служб.

4.5. Выводы.

Введение диссертации (часть автореферата) на тему «Автоматизация проектирования и верификации межмодульных интерфейсов информационных систем на основе операторного моделирования»

Актуальность темы

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

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

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

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

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

Работа выполнена в соответствии с научным направлением ЛГТУ "Информационные системы и базы данных".

Цель работы

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

Задачи исследования

Для достижения поставленной цели необходимо решить следующие задачи:

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

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

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

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

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

Методы исследования

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

Научная новизна работы

К результатам работы, отличающимся научной новизной, относятся:

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

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

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

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

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

Практическая значимость работы

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

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

Результаты внедрения

Результаты исследований апробированы при проектировании специализированных информационных систем "ГУК Правобережная" (г.Липецк), издательства «Научная книга» (г.Воронеж), а также в учебном процессе Липецкого государственного технического университета на кафедре «Прикладная математика».

Апробация работы

Основные положения диссертации докладывались и обсуждались на: XII-й Международной открытой научной конференции «Современные проблемы информатизации в моделировании и анализе сложных систем» (Воронеж, 2007), XIII-й и XIV-й Международной открытой научной конференции «Современные проблемы информатизации в моделировании и социальных технологиях» (Воронеж, 2008, Орел, 2009), XIII-й Международной открытой научной конференции «Современные проблемы информатизации в проектировании и информационных системах» (Воронеж, 2008), Всероссийской конференции «Новые технологии в научных исследованиях, проектировании, управлении, производстве» (Воронеж, 2008); XIV-й Международной открытой научной конференции «Современные проблемы информатизации в анализе и синтезе программных и телекоммуникационных систем» (Орел, 2009), научно-тематическом семинаре ЛГТУ "Информационные системы и базы данных" (Липецк, 2007-2009).

Публикации

По материалам диссертации опубликовано 12 научных работ, в том числе 5 - в изданиях, рекомендованных ВАК РФ. В работах, опубликованных в соавторстве и приведенных в конце автореферата, лично соискателю принадлежат: в [2, 8, 9] - метод формального анализа проектных решений по реализации механизмов межмодульного взаимодействия; в [7, 10] -способ анализа конкретного операторного выражения на принадлежность классу нормированных прямых отображений; в [1, 5, 6] - алгоритм синтеза проектных решений по реализации межмодульного взаимодействия; в [4, 9, 10] - алгоритм верификации межмодульного взаимодействия как основы принятия корректирующих проектных решений; в [3, 4, 11, 12] - элементы математического и лингвистического обеспечения подсистемы анализа и синтеза проектных решений по верификации результатов проектирования межмодульных интерфейсов.

Структура и объем работы

Диссертация состоит из введения, четырех глав, заключения, списка литературы из 105 наименований. Основная часть работы изложена на 149 страницах, содержит 3 таблицы и 37 рисунков.

Заключение диссертации по теме «Системы автоматизации проектирования (по отраслям)», Корчагин, Александр Сергеевич

4.5. Выводы

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

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

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

Заключение

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

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

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

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

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

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

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

В процессе исследования получены следующие результаты, отличающиеся научной новизной:

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

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

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

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

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

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

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

Результаты исследований апробированы при проектировании специализированных информационных систем "ГУК Правобережная" (г.Липецк), издательства «Научная книга» (г.Воропеж), а также в учебном процессе Липецкого государственного технического университета на кафедре «Прикладная математика».

Таким образом, в процессе выполнения диссертационного исследования были получены следующие основные результаты:

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

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

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

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

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

6. На основе предложенных методов и алгоритмов в процессе автоматизированного проектирования верифицирован ряд компонентов информационных систем, практическая апробация которых подтвердила корректную проектную верификацию.

Список литературы диссертационного исследования кандидат технических наук Корчагин, Александр Сергеевич, 2009 год

1. Авен О.И., Гурнн Н.Н., Коган Я.А. Оценка качества и оптимизация вычислительных систем. — М.: Наука, 1982.

2. Анализ и синтез сложных технических систем. В 2-х ч., 4.1. М.: Воениздат, 1995.-401 с.

3. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. В 2-х томах. М.: Мир. 1978.

4. Байцер Б. Архитектура вычислительных комплексов. Том 1. М.: Мир. 1974.

5. Баранов С.И. Синтез микропрограммных автоматов. Л.: Энергия. -1979.

6. Бек К. Экстремальное программирование. Библиотека программиста. СПб.: Питер, 2002. - 224 с.

7. Боггс У., Боггс М. UML и Rational Rose. М.: Лори, 2001. - 608 с.

8. Брукс Ф. Мифический человеко-месяц, или как создаются программные системы,- СПб.: Символ-Плюс, 2005.-304 с.

9. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++. М.: "Изд-во Бином", СПб: "Невский диалект". 1998.

10. Буч Г., Рамбо Д., Джскобсон А. Язык UML. Руководство пользователя. М.: ДМК.-2000.

11. П.Говорский А.Э. Распределенные информационные системы контроля и управления. СПб: Энергоатомиздат, Санкт-Петербургское отделение, 2004. - 378 с.

12. Говорский А.Э., Жданов Н.Ф., Корчагин А.С. Математическая модель гетерогенной интегральной корпоративной информационно-управляющей системы в дискретном времени// Системы управления и информационные технологии. №1.1(35), 2009. С. 139-144.

13. Говорский А.Э., Жданов Н.Ф., Корчагин А.С. Проектированиепрограммной системы идентификации характеристик неоднородных систем с интеграцией служб// Системы управления и информационные технологии, 2009, 2.1(36) С. 204-208.

14. Говорский А.Э., Корчагин А.С., Кравец О.Я. Параметрический синтез гетерогенной интегральной корпоративной информационно-управляющей системы// Системы управления и информационные технологии. №3.1(33), 2008. С. 128-134.

15. Говорский А.Э., Кравец О.Я. Математическое моделирование неоднородного трафика гетерогенной интегральной корпоративной информационно-управляющей системы// Системы управления и информационные технологии. №2.2(32), 2008. С. 228-234.

16. Говорский А.Э., Кравец О.Я., Повалясв А.Д. Подходы к моделированию неоднородных интегральных информационно-управляющих систем// Системы управления и информационные технологии, 2007, №3.1(29). -С. 131-138.

17. Говорский А.Э., Кравец О.Я., Суворов Д.В. Проблемы и особенности моделирования и рационального проектирования интегральных систем обслуживания неоднородного трафика// Системы управления и информационные технологии, 2007, №2.1(28). С. 122-129.

18. Гуров В., Нарвский А., Шалыто А. Исполняемый UML из России //PC Week/RE. 2005. - № 26. - С. 18-19.

19. Джамп Д. AutoCAD. Программирование. М.: Радио и связь.1992.

20. Константин JI. Человеческий фактор в программировании. СПб.: Символ-Плюс, 2004. - 384 с.

21. Корбут А.А., Финкелыптейн Ю.Ю. Приближенные методы дискретного программирования. // Изв. АН СССР: Техн. Кибернетика, 1963, №1. С. 165-176.

22. Корчагин А.С., Кравец О.Я. О состоянии проблемы проверки корректности систем и протоколов// Современные проблемы информатизации в моделировании и анализе сложных систем: Сб. тр. Вып. 13. Воронеж: Научная книга, 2007. - С. 198-207.

23. Корчагин А.С., Кравец О.Я. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714-719.

24. Корчагин А.С., Кравец О.Я., Погодаев А.К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, №3.1(29). С. 166-169. 2.2.4.

25. Корчагин А.С., Свиридова О.С., Кравец О.Я. Особенности разработки и верификации программного обеспечения системы управления научным журналом// Информационные технологии моделирования, и управления, № 4(56), 2009. С. 492-502.

26. Корчагин А.С., Погодаев А.К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186-195.

27. Корчагин А.С., Погодаев А.К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186-195.

28. Корчагин А.С., Погодаев А.К. К методологии операторного моделирования при исследовании корректности программ// Информационные технологии моделирования и управления, №3(37), 2007. С. 363-370.

29. Корчагин А.С., Погодаев А.К. О связи нормированных прямых и обратных отображений// Системы управления и информационные технологии, 2008, 3.2(33). С. 283-287.

30. Корчагин А.С., Погодаев А.К. Основы применения нормированных моделей для доказательства корректности программ// Информационные технологии моделирования и управления, № 6(31), 2006. С. 731-738.

31. Корчагин А.С., Погодаев А.К. Программная реализация комплекса для проведения вычислительного эксперимента по анализу плана ремонтных работ// Информационные технологии моделирования и управления, № 4(56), 2009. С. 605-612.

32. Корчагин А.С., Погодаев А.К. Технология пошаговой детализации при операторном моделировании для доказательства корректности программ// Территория науки, 2007, №4(5). Воронеж 2007. С. 501-507.

33. Кравец О.Я., Корчагин А.С. О связи прямого и нормированного прямого отображений// Информационные технологии моделирования и управления, 2008, №4(47). С. 392-398.

34. Кравец О.Я., Корчагин А.С. Об особенностях нормированных обратных отображений// Информационные технологии моделирования и управления, № 7(50), 2008. С. 796-803.

35. Кравец О.Я., Корчагин А.С. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714-719.

36. Кравец О.Я., Корчагин А.С., Погодаев А.К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, №3.1(29). С. 166-169.

37. Кравец О.Я., Корчагин А.С., Погодаев А.К. О свойствах нормированного прямого моделирования, использующего пошаговую детализацию// Информационные технологии моделирования и управления, № 9(43), 2007.-С. 1037-1041.

38. Кравец О.Я., Корчагин А.С., Погодаев А.К. О свойствах обратных отображений с ветвлениями. Современные проблемы информатизации в моделировании и социальных технологиях: Сборник трудов, выпуск 14. -Воронеж: «Научная книга», 2009. - С. 236-239.

39. Кравец О.Я., Свиридова О.С. Система управления Web-контентом "Научный журнал" // Информационные технологии моделирования и управления / Международный сборник научных трудов. Выпуск 15. Воронеж: Изд-во "Научная книга", 2003. - с. 61-65.

40. Кремер А.А, Корчагин А.С. Программный модуль «Модель многоуровневой реконфигурируемой системы». М.: ФАП ВНТИЦ, 2007. № ГР 50200701849 от 30.08.07.

41. Кузнецов Б.П. Стандартная реализация управляющих программ // Судостроительная промышленность. Сер. Системы автоматизированного проектирования 1986. с. 51 - 55.

42. Кузнецов О.П., Адельсон-Вельский Г.М. Дискретная математика для инженера. М.: Энергоатомиздат. 1988.

43. Маракушин М.В. Задача перспективного планирования ремонтно-восстановительных работ // Управление большими системами. 2006. -Вып. 14. С. 140-146.

44. Маракушин М.В., Томилов A.J1. Информационная система управления жилищным фондом // Системы управления и информационные технологии, 2007. № 1.1(27). С. 176-180.

45. Мартин Дж. Вычислительные сети и распределенная обработка данных: программное обеспечение, методы и архитектура. Вып. 1. - М.: Финансы и статистика, 1985. - 256 с.

46. Системное проектирование интегрированных программных комплексов. / Под ред. В.М. Пономарева. Д.: Машиностроение, 1996. - 336 с.

47. Срибнер JI.A. Программируемые устройства автоматики. К.: Технжа. 1982.

48. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 1 // Компоненты и технологии. 2006. №11.

49. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 2 // Компоненты и технологии. 2006. №12.

50. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 3 // Компоненты и технологии. 2007. №1.

51. Фаулер М. UML. СПб.: Символ-Плюс, 2004. - 192 с.

52. Шалыто А.А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука. 1998.

53. Шалыто А.А. Алгоритмизация и программирование задач логического управления. СПб.: СПбГУ ИТМО. - 1998. - 56 с.

54. Шалыто А.А. Еще раз об открытой проектной документации //PC Week/RE. 2005. - № 11, - С. 33-34.

55. Шалыто А.А. Использование граф-схем и графов переходов при программной реализации алгоритмов логического управления //Автоматика и телемеханика. 1996, - № 6. - С. 148 - 158; № 7. - С. 144— 169.

56. Шалыто А.А. Логическое управление. Методы аппаратной и программной реализации. СПб.: Наука, 2000. - 780 с.

57. Шалыто А.А. Новая инициатива в программировании. Движение за открытую проектную документацию //Мир компьютерной автоматизации. 2003. -№ 5. - С.67-71.

58. Шалыто А.А. Программная реализация управляющих автоматов// Судостроительная промышленность. Сер. «Автоматика и телемеханика». 1991. Вып. 13, с. 41-42.

59. Шеннон Р. Имитационное моделирование систем искусство и наука. - М.: Мир, 1988. - 634 с.

60. Шнейдерман Б. Психология программирования. М.: Радио и связь. 1984.

61. Abadi М., Lamport L. The existence of refinement mappings. Theoretical Computer Science, 82(2):253-284, 1991.

62. Bensalem Saddek, Ganesh Vijay, Lakhnech Yassine, et al. An overview of SAL. In C. Michael Iiolloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187-196, Hampton, VA, jun 2000. NASA Langley Research Center.

63. Browne M.C., Clarke E.M., Grumberg O. Characterizing finite Kripke structures in Prepositional temporal logic. Theoretical Computer Science, 59(1,2):115-131, 1988.

64. Devillers M.C.A., Grioen W.O.D., Romijn J.M.T, Vaandrager F.W. Verification of a leader election protocol: Formal methods applied to IEEE 1394. Formal Methods in System Design, 16(3):307-320, June 2000.

65. Garland S.J., Lynch N.A., Vaziri M. IOA: A language for specifying, programming, and validating distributed systems, 1997. http://larch. lcs.mit.edu: 800 l/~garland/ioaLanguage. html.

66. Gawliclc R., Segala R., Sogaard-Andersen J.F., Lynch N.A. Liveness in timed and untimed systems. Technical ReportMIT/LCS/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993.

67. Ginzburg A. Algebraic Theory of Automata. Academic Press, New York-London, 1968.

68. Glabbeek R.J., Weijland W.P. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996.

69. Grioen W.O.D. Studies in Computer Aided Verification of Protocols. PhD thesis, University of Nijmegen, May 2000. Postscript and PVS sources available via http://www.cs.lam.nl/ita/former members/davidg/.

70. Groote J.F., Springintveld J.S. Focus points and convergent process operators — a Proof strategy for protocol verification. Report CS-R9566, Department of Software Technology, CWI, Amsterdam, November 1995. 1.3.10.

71. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.

72. Harel D. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming. 1987. Vol. 8, P. 231 -274.

73. Jonsson B. A model and Proof system for asynchronous networks. In Proceedings of the 4th Annual ACM Symposium on Principles of Distributed Computing, Minaki, Ontario, Canada, pages 49-58, 1985.

74. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.

75. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.

76. Jonsson B. Simulations between specifications of distributed systems. In J.C.M. Baeten and J.F. Groote, editors, Proceedings CONCUR 91, Amsterdam, volume 527 of Lecture Notes in Computer Science, pages 346-360. Springer-Verlag, 1991.

77. Klarlund N., Schneider F.B. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1): 151—170, November 1993.

78. Klarlund N., Schneider F.B. Verifying safety properties using infinite-state automata. Technical Report 89-1039, Department of Computer Sci-~ ence, Cornell University, Ithaca, New York, 1989.

79. Knuth D.E. Fundamental Algorithms, volume 1 of The Art of Computer Programming. Addison-Wesley, Reading, Massachusetts, 1997. Third edition.

80. Lamport L. What good is temporal logic? In R.E. Mason, editor, Information Processing 83, pages 657-668. North-Holland, 1983.

81. Lynch N.A. Distributed Algorithms. Morgan Kaufmann Publishers, Inc., San Fransisco, California, 1996.

82. Lynch N.A., Vaandrager F.W. Forward and backward simulations, I: Untimed systems. Information and Computation, 121(2):214-233, September 1995.

83. Manna Z., Browne A., Sipma H.B., Uribe Т.Е. Visual abstraction for temporal verification. In A.M. Haebercr, editor, Proceedings AMAST'98, volume 1548 of Lecture Notes in Computer Science, pages 28-41. Springer-Verlag, 1998.

84. Mueller О. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technical University of Munich, September 1998.

85. Nicola R. and Vaandrager F.W. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, March 1995.

86. Nipkow Т., Slind K. I/O automata in Isabelle/PIOL. In P. Dybjer, B. Nordstrom, and J. Smith, editors, Types for Proof and Programs, volume 996 of Lecture Notes in Computer Science, pages 101-119. Springer-Verlag, 1995.

87. Owicki S., Grics D. An axiomatic Proof technique for parallel programs. Acta Informatica, 6(4):319-340, 1976.

88. Roever W.P., Engelhardt K. Data Refinement: Model-Oriented Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. Cambridge University Press, 1998.

89. Sogaard-Andersen J.F., Lynch N.A., Lampson B.W. Correctness of communication protocols a case study. Technical Report MIT/LCS/TR-589, Laboratory for Computer Science, MIT, Cambridge, MA, November 1993.

90. Stark E.W. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135-154, 1988.

91. Wolper Pierre. The meaning of formal: from weak to strong formal methods. Springer International Journal on Software Tools for Technology Transfer, l(l-2):6-8, 1997. 1.3.35.