Помощь в написании студенческих работ
Антистрессовый сервис

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

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

По материалам диссертации опубликовано 12 научных работ, в том числе 5 — в изданиях, рекомендованных ВАК РФ. В работах, опубликованных в соавторстве и приведенных в конце автореферата, лично соискателю принадлежат: в — метод формального анализа проектных решений по реализации механизмов межмодульного взаимодействияв -способ анализа конкретного операторного выражения на принадлежность классу… Читать ещё >

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

Содержание

  • 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. На основе предложенных методов и алгоритмов в процессе автоматизированного проектирования верифицирован ряд компонентов информационных систем, практическая апробация которых подтвердила корректную проектную верификацию.

Показать весь текст

Список литературы

  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. А.С., Кравец О. Я. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714−719.
  23. А.С., Кравец О. Я., Погодаев А. К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, № 3.1(29). С. 166−169. 2.2.4.
  24. А.С., Свиридова О. С., Кравец О. Я. Особенности разработки и верификации программного обеспечения системы управления научным журналом// Информационные технологии моделирования, и управления, № 4(56), 2009. С. 492−502.
  25. А.С., Погодаев А. К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186−195.
  26. А.С., Погодаев А. К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186−195.
  27. А.С., Погодаев А. К. К методологии операторного моделирования при исследовании корректности программ// Информационные технологии моделирования и управления, № 3(37), 2007. С. 363−370.
  28. А.С., Погодаев А. К. О связи нормированных прямых и обратных отображений// Системы управления и информационные технологии, 2008, 3.2(33). С. 283−287.
  29. А.С., Погодаев А. К. Основы применения нормированных моделей для доказательства корректности программ// Информационные технологии моделирования и управления, № 6(31), 2006. С. 731−738.
  30. А.С., Погодаев А. К. Программная реализация комплекса для проведения вычислительного эксперимента по анализу плана ремонтных работ// Информационные технологии моделирования и управления, № 4(56), 2009. С. 605−612.
  31. А.С., Погодаев А. К. Технология пошаговой детализации при операторном моделировании для доказательства корректности программ// Территория науки, 2007, № 4(5). Воронеж 2007. С. 501−507.
  32. О.Я., Корчагин А. С. О связи прямого и нормированного прямого отображений// Информационные технологии моделирования и управления, 2008, № 4(47). С. 392−398.
  33. О.Я., Корчагин А. С. Об особенностях нормированных обратных отображений// Информационные технологии моделирования и управления, № 7(50), 2008. С. 796−803.
  34. О.Я., Корчагин А. С. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714−719.
  35. О.Я., Корчагин А. С., Погодаев А. К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, № 3.1(29). С. 166−169.
  36. О.Я., Корчагин А. С., Погодаев А. К. О свойствах нормированного прямого моделирования, использующего пошаговую детализацию// Информационные технологии моделирования и управления, № 9(43), 2007.-С. 1037−1041.
  37. Кремер А. А, Корчагин А. С. Программный модуль «Модель многоуровневой реконфигурируемой системы». М.: ФАП ВНТИЦ, 2007. № ГР 50 200 701 849 от 30.08.07.
  38. .П. Стандартная реализация управляющих программ // Судостроительная промышленность. Сер. Системы автоматизированного проектирования 1986. с. 51 — 55.
  39. О.П., Адельсон-Вельский Г.М. Дискретная математика для инженера. М.: Энергоатомиздат. 1988.
  40. М.В. Задача перспективного планирования ремонтно-восстановительных работ // Управление большими системами. 2006. -Вып. 14. С. 140−146.
  41. М.В., Томилов A.J1. Информационная система управления жилищным фондом // Системы управления и информационные технологии, 2007. № 1.1(27). С. 176−180.
  42. Дж. Вычислительные сети и распределенная обработка данных: программное обеспечение, методы и архитектура. Вып. 1. — М.: Финансы и статистика, 1985. — 256 с.
  43. Системное проектирование интегрированных программных комплексов. / Под ред. В. М. Пономарева. Д.: Машиностроение, 1996. — 336 с.
  44. JI.A. Программируемые устройства автоматики. К.: Технжа. 1982.
  45. В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 1 // Компоненты и технологии. 2006. № 11.
  46. В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 2 // Компоненты и технологии. 2006. № 12.
  47. В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 3 // Компоненты и технологии. 2007. № 1.
  48. Фаулер М. UML. СПб.: Символ-Плюс, 2004. — 192 с.
  49. Шалыто А.А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука. 1998.
  50. А.А. Алгоритмизация и программирование задач логического управления. СПб.: СПбГУ ИТМО. — 1998. — 56 с.
  51. А.А. Еще раз об открытой проектной документации //PC Week/RE. 2005. — № 11, — С. 33−34.
  52. А.А. Использование граф-схем и графов переходов при программной реализации алгоритмов логического управления //Автоматика и телемеханика. 1996, — № 6. — С. 148 — 158- № 7. — С. 144— 169.
  53. А.А. Логическое управление. Методы аппаратной и программной реализации. СПб.: Наука, 2000. — 780 с.
  54. А.А. Новая инициатива в программировании. Движение за открытую проектную документацию //Мир компьютерной автоматизации. 2003. -№ 5. — С.67−71.
  55. А.А. Программная реализация управляющих автоматов// Судостроительная промышленность. Сер. «Автоматика и телемеханика». 1991. Вып. 13, с. 41−42.
  56. Р. Имитационное моделирование систем искусство и наука. — М.: Мир, 1988. — 634 с.
  57. . Психология программирования. М.: Радио и связь. 1984.
  58. Abadi М., Lamport L. The existence of refinement mappings. Theoretical Computer Science, 82(2):253−284, 1991.
  59. 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.
  60. 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.
  61. 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.
  62. 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.
  63. 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.
  64. Ginzburg A. Algebraic Theory of Automata. Academic Press, New York-London, 1968.
  65. Glabbeek R.J., Weijland W.P. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555−600, 1996.
  66. 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/.
  67. 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.
  68. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
  69. Harel D. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming. 1987. Vol. 8, P. 231 -274.
  70. 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.
  71. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.
  72. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.
  73. 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.
  74. Klarlund N., Schneider F.B. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1): 151—170, November 1993.
  75. 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.
  76. Knuth D.E. Fundamental Algorithms, volume 1 of The Art of Computer Programming. Addison-Wesley, Reading, Massachusetts, 1997. Third edition.
  77. Lamport L. What good is temporal logic? In R.E. Mason, editor, Information Processing 83, pages 657−668. North-Holland, 1983.
  78. Lynch N.A. Distributed Algorithms. Morgan Kaufmann Publishers, Inc., San Fransisco, California, 1996.
  79. Lynch N.A., Vaandrager F.W. Forward and backward simulations, I: Untimed systems. Information and Computation, 121(2):214−233, September 1995.
  80. 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.
  81. Mueller О. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technical University of Munich, September 1998.
  82. Nicola R. and Vaandrager F.W. Three logics for branching bisimulation. Journal of the ACM, 42(2):458−487, March 1995.
  83. 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.
  84. Owicki S., Grics D. An axiomatic Proof technique for parallel programs. Acta Informatica, 6(4):319−340, 1976.
  85. Roever W.P., Engelhardt K. Data Refinement: Model-Oriented Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. Cambridge University Press, 1998.
  86. 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.
  87. Stark E.W. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135−154, 1988.
  88. 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.
Заполнить форму текущей работой

Сессия? Спокойно!