Спецкурс "Математические методы описания и анализа систем"

Лектор: исп. об. мл. научн. сотр. ИСП РАН Жуков Д.Ю.
E-mail:

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

В начале курса излагается метод индуктивных утверждений Флойда, при помощи которого можно доказывать правильность последовательных программ. В остальной части курса рассматриваются главным образом распределенные системы, то есть системы, состоящие из нескольких параллельно работающих компонент. В курсе даются сведения о формальных моделях, при помощи которых можно описывать такие системы. К числу этих моделей относятся Исчисление Взаимодействующих Систем (CCS) и -исчисление. Слушатель знакомится как с результатами теоретического программирования, так и с примерами применения этих результатов для описания, анализа и доказательства правильности простых систем.

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

Спецкурс рекомендован для студентов 2-5 курсов.

Ресурсы:

Страница спецкурса на сайте Института Системного программирования РАН URL: http://case.ispras.ru/mmoas/. На ней опубликованы конспекты лекций.

Программа курса

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

Блок-схемы. Спецификация блок-схем при помощи пред- и постусловий.
Верификация (доказательство правильности) блок-схем методом индуктивных утверждений Флойда.
Примеры доказательства правильности блок-схем.

II. Описание поведения распределенных систем и их анализ при помощи процессных графов. Проверка эквивалентности двух систем и минимизация систем.

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

III. Исчисление взаимодействующих систем (The Calculus of Communicating Systems, CCS). Его применение: эквивалентные преобразования и верификация систем.

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

IV. Описание систем с мобильными компонентами при помощи

-исчисления.

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

Примечание: планируемый порядок изложения тем в спецкурсе не везде совпадает с данным планом.

Литература:

G.Bruns, Distributed systems analysis with CCS, Prentice-Hall, 1997.
R.Milner, Communication and concurrency, Prentice-Hall, 1989.
R.Milner, Operational and algebraic semantics of concurrent processes, In Handbook of Theoretical Computer Science, volume B, chapter 9, Elsevier Science Publishers B.V., 1990.
R.Milner, Communicating and mobile systems: The -calculus, Cambridge University Press, 1999.
Ч.Хоар, Взаимодействующие последовательные процессы, Москва, "Мир", 1985.