Перейти к полному списку специальных курсов кафедры

Программа спецкурса "Математическая теория программирования"

1. Главная задача курса

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

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

Основными учебными пособиями по данному спецкурсу являются подготовленные автором тексты

1). А.М.Миронов, Математическая теория программных систем [1], и

2). А.М.Миронов, Математическая логика [2].

2. Актуальность

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

Требования к качеству систем отражены в стандарте [5]. Отметим наиболее важные из них.

1. Корректность, т.е. соответствие системы своему предназначению.

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

3. Устойчивость системы в случае непредусмотренного поведения окружения и при работе с неправильными входными данными.

4. Эффективность использования ресурсов времени и памяти. Оптимальность реализованных в системе алгоритмов.

5. Адаптируемость системы к небольшим изменениям окружения путём изменения её настроек, без изменения её внутренней структуры.

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

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

Как правило, анализ соответствия системы предъявляемым к ней требованиям производится методом тестирования.

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

Рассмотрим эти методы подробнее.

2.1 Тестирование

Тестирование системы заключается в анализе её поведения на некоторых выборочных входных данных.

Тестирование является в настоящее время основной формой контроля качества систем, и занимает примерно две трети общего времени, затрачиваемого на их разработку.

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

Как отметил Дейкстра ([6], стр. 41), тестирование может лишь помочь выявить некоторые ошибки, но отнюдь не доказать их отсутствие.

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

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

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

2.2 Верификация

Верификация системы состоит из следующих частей.

1. Построение математической модели анализируемой системы.

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

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

Как правило, верификация применяется для анализа первого требования к системе – её корректности. Отметим, что это требование является главным, т.к. в случае его нарушения эксплуатация системы невозможна, даже если она удовлетворяет всем остальным требованиям.

3. Автоматные модели систем

Автоматная модель системы представляет собой граф,

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

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

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

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

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

1). Автоматная модель системы не должна быть чрезмерно детальной, т.к. излишняя сложность модели может вызвать существенные вычислительные проблемы при её формальном анализе.

2). Автоматная модель системы не должна быть чрезмерно упрощённой, она должна

- отражать те аспекты системы, которые имеют отношение к проверяемым свойствам, и

- сохранять все свойства моделируемой системы, представляющие интерес для анализа,

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

В литературе по теоретическому программированию исследуются различные классы автоматных моделей систем (которые обычно называются расширенными автоматами). В спецкурсе будут изложены следующие автоматные модели:

1). введённая автором в [3] автоматная модель, предназначенная для формального представления нерекурсивных последовательных и параллельных программ, а также

2). введённая автором в [4] автоматная модель, предназначенная для формального представления функциональных программ.

4. Алгебраические модели систем

Для описания алгебраических моделей систем в спецкурсе будет излагаться алгебраический язык исчисления взаимодействующих систем, введённый Р. Милнером [9], и изначально предназначенный для описания параллельных программ и сложных структур данных, но затем нашедший важные применения также для описания моделей и свойств криптографических протоколов [10], и бизнес-процессов.

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

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

5. Спецификация программных систем

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

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

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

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

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

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

Поэтому для представления свойства системы в виде спецификации важно выбрать такой ЯС, на котором спецификация этого свойства имела бы наиболее ясный и простой вид.

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

6. Построение доказательств

Существует два основных метода построения формального доказательства того, что модель программной системы удовлетворяет или не удовлетворяет спецификации этой системы:

1). model checking [7], использование которого даёт наибольший эффект в том случае, когда модель не удовлетворяет спецификации, и

2). логический вывод ([1], [8]), который более эффективен (по сравнению с model checking) для обоснования того, что модель удовлетворяет спецификации.

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

6.1 Model checking

Model checking представляет собой автоматический анализ модели, которая может быть задана

- либо явно, путём перечисления всех состояний и соединяющих их рёбер,

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

Если модель не удовлетворяет спецификации, то в качестве доказательства этого факта model checking предъявляет опровергающее вычисление, т.е. последовательность действий модели, на которой нарушается эта спецификация.

6.2 Логический вывод

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

- инварианты истинны в начальный момент работы системы

- инварианты сохраняют свою истинность после каждого шага работы системы, и

- из конъюнкции данных инвариантов следует спецификация системы.

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

1). Блок-схемы последовательных программ и их автоматные модели.

2). Метод Флойда для верификации последовательных программ.

3). Логика Хоара для верификации последовательных программ.

4). Автоматные модели параллельных программ.

5). Логические методы верификации параллельных программ.

6). Алгебраические операции на программах. Исчисление взаимодействующих систем.

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

8). Алгебраические методы верификации программ.

9). Логические методы верификации функциональных программ.

10). Алгебраические методы описания и верификации криптографических протоколов методами pi-исчисления.

11). Темпоральная логика линейного и ветвящегося времени.

12). Описание метода model checking для темпоральной логики ветвящегося времени.

13). Описание метода model checking для темпоральной логики линейного времени.

14). Символьные методы верификации.

15). Методы редукции систем переходов для понижения сложности задачи верификации.

Литература.

[1] А.М.Миронов: Математическая теория программных систем.

[2] А.М.Миронов: Математическая логика.

[3] Миронов А.М., Жуков Д.Ю.: Математическая модель и методы верификации программных систем. Интеллектуальные системы, том. 9, 2005, Москва, стр. 209-252

[4] Миронов А.М.: Верификация функциональных программ на основе построения их графовых моделей. Труды IX международной конференции "Интеллектуальные системы и компьютерные науки", 23-27 октября, 2006, Московский гос. университет им. М.В.Ломоносова, том. 2, стр 207-211

[5] International Standard ISO/IEC 9126. Information Technology – Software Product Evaluation – Quality Characteristics and Guidelines for their Use. International Organization for Standardization, International Electrotechnical Commission, Geneva, 1991.

[6] Лекции лауреатов премии Тьюринга. Москва, Мир, 1993.

[7] E. Clarke, O. Grumberg, D. Peled: Model checking. MIT Press, 2001.

[8] R.W.Floyd: Assigning meanings to programs, Proc. Symp. Appl. Math., 19; in: J.T.Schwartz (ed.), Mathematical Aspects of Computer Science, pp. 19-32, American Mathematical Society, Providence, R.I., 1967.

[9] R.Milner: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92, Springer, 1980.

[10] Abadi M., Gordon A.: A Calculus for Cryptographic Protocols: The Spi Calculus, Proceedings of the Fourth ACM Conference on Computers and Communications Security, (1997) 36-47, ACM Press.

Наверх