МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ

РОССИЙСКОЙ ФЕДЕРАЦИИ

Ярославский государственный университет им. П.Г. Демидова

Факультет информатики и вычислительной техники

УТВЕРЖДАЮ

Проректор по развитию образования

_Е.В. Сапир "_"2012 г.

Рабочая программа дисциплины послевузовского профессионального образования (аспирантура) Моделирование и анализ информационных систем по специальности научных работников 05.13.11 Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Ярославль 1. Цели освоения дисциплины Целями освоения дисциплины «Моделирование и анализ информационных систем» в соответствии с общими целями основной профессиональной образовательной программы послевузовского профессионального образования (аспирантура) (далее ОПП – образовательная программа послевузовского профессионального образования) являются:

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

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

Дисциплина «Моделирование и анализ информационных систем» необходима для решения задач построения информационных систем, анализа и исследования различных свойств информационных систем и их моделей.

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

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

3. Требования к результатам освоения содержания дисциплины В результате освоения дисциплины обучающийся должен:

Знать:

1) способы моделирования информационных систем;

2) способы спецификации и анализа свойств информационных систем;

3) способы обеспечения корректного функционирования информационных систем;

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

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

Уметь:

1) проводить спецификацию систем на формальном языке;

2) применять формальные методы для доказательства корректности систем;

3) строить программные модели и проводить спецификацию и верификацию программных свойств;

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

Владеть:

1) методами моделирования и спецификации систем;

2) методами анализа информационных систем (программ).

4. Структура и содержание дисциплины «Моделирование и анализ информационных систем»

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

Курс Неделя № Раздел Виды учебной работы, Формы текущего контроля Раздел 1. Принципы и технические средства верификации систем. Системы автоматов. Синхронизированное произведение. Синхронизация посредством сообщений.

Синхронизация посредством общих переменных. Темпоральная логика. Язык темпоральной логики. Формальные синтаксис и семантика темпоральной логики. Логики PLTL и CTL. Выразительность логики CTL*.

Раздел 2. Model-checking в логиках CTL и PLTL. Проблема экспоненциального роста числа состояний. Символический Model-checking. Символическое представление множеств состояний. Бинарные диаграммы решений (БДР). Представление автоматов посредством БДР. Model-checking на основе БДР. Временные автоматы. Сеть временных автоматов и синхронизация. Расширения базовой модели. Временная темпоральная логика. Временной Model-checking.

Раздел 3. Свойства достижимости. Достижимость в темпоральной логике. Modelchecking и достижимость. Построение графа достижимости. Свойства безопасности в темпоральной логике. Свойства безопасности на практике. Свойства живости в темпоральной логике. Верификация в предположении живости. Ограниченная живость.

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

Раздел 4. SMV - символический Model-checking. Назначение и особенности SMV.

Описание автоматов. Верификация. Синхронизация автоматов. Документирование и рассмотрение отдельных случаев. Spin - коммуникативные автоматы. Назначение и особенности Spin. Описание процессов. Моделирование системы. Верификация.

Документирование и рассмотрение отдельных случаев. Design/CPN - раскрашенные сети Петри. Назначение и свойства. Редактор. Моделирование сети. Анализ сети.

Документирование и рассмотрение отдельных случаев. Uppaal - системы со временем.

Назначение и свойства Uppaal. Описание автоматов. Моделирование системы.

Верификация. Документирование и рассмотрение отдельных случаев. Kronos - временной Model-checking. Назначение и свойства Kronos’а. Описание автоматов.

Синхронизированное произведение. Model-checking. Документирование и рассмотрение отдельных случаев. HyTech - линейные гибридные системы. Назначение и особенности HyTech. Описание автоматов. Анализ системы и анализ параметров. Документирование и рассмотрение отдельных случаев.

5. Образовательные технологии В основу образовательной технологии по дисциплине «Моделирование и анализ информационных систем» помимо традиционных форм занятий в виде лекций положена также форма, состоящая в выполнении аспирантом индивидуальных заданий по темам дисциплины. Имеются четыре индивидуальных задания по дисциплине. Задания должны быть решены письменно или в электронном виде с последующей устной защитой. Первое задание закрывает тематику дедуктивного анализа корректности последовательных программ. Представляет собой небольшую программу, написанную на «простом» языке высокого уровня, корректность которой необходимо доказать относительно спецификации, составляемой аспирантом по словесному описанию требований к программе. При безуспешных со стороны аспиранта попытках построения инварианта, ограничивающей функции и постусловия эти необходимые для выполнения задания компоненты могут быть предоставлены обучающемуся. Выполнение второго, третьего и четвертого заданий предполагает моделирование (представление в виде структуры Крипке), спецификацию (запись свойств на языке темпоральной логики) и автоматическую верификацию некоторой параллельной и распределенной программы с помощью свободно распространяемых для учебных целей средств верификации SPIN, SMV и Uppaal. Ошибки, допущенные при выполнении задания, отмечаются подробно преподавателем, ведущим дисциплину. После исправления ошибок задание сдается вновь преподавателю на проверку. Аспиранты, сдавшие все индивидуальные задания в установленные сроки, после успешного ответа на ряд дополнительных вопросов, закрывающих оставшиеся темы, получают отметку о сдаче зачета досрочно. Такой подход стимулирует постоянную работу аспирантов и активизирует усвоение материала. Эта технология позволяет проводить индивидуальное обучение аспирантов и дает хорошие результаты. Она дополняется обсуждением общих (типичных) ошибок на лекционных занятиях.

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

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

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

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

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

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

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

1. Принципы и технические средства верификации систем.

2. Системы автоматов. Синхронизированное произведение. Синхронизация посредством сообщений. Синхронизация посредством общих переменных.

3. Темпоральная логика. Язык темпоральной логики. Формальные синтаксис и семантика темпоральной логики. Логики PLTL и CTL. Выразительность логики CTL*.

4. Model-checking в логиках CTL и PLTL. Проблема экспоненциального роста числа состояний.

5. Символический Model-checking. Символическое представление множеств состояний.

Бинарные диаграммы решений (БДР). Представление автоматов посредством БДР. Modelchecking на основе БДР.

6. Временные автоматы. Сеть временных автоматов и синхронизация. Расширения базовой модели. Временная темпоральная логика. Временной Model-checking.

7. Свойства достижимости. Достижимость в темпоральной логике. Model-checking и достижимость. Построение графа достижимости.

8. Свойства безопасности в темпоральной логике. Свойства безопасности на практике.

9. Свойства живости в темпоральной логике. Верификация в предположении живости.

Ограниченная живость.

10. Отсутствие блокировки в автомате. Связь безопасностью и живостью.

11. Методы абстракции. Абстракция посредством слияния состояний. Абстракция на основе переменных. Абстракция с помощью ограничений.

12. SMV - символический Model-checking. Назначение и особенности SMV. Описание автоматов. Верификация. Синхронизация автоматов. Документирование и рассмотрение отдельных случаев.

13. Spin - коммуникативные автоматы. Назначение и особенности Spin. Описание процессов. Моделирование системы. Верификация. Документирование и рассмотрение отдельных случаев.

14. Design/CPN - раскрашенные сети Петри. Назначение и свойства. Редактор.

Моделирование сети. Анализ сети. Документирование и рассмотрение отдельных случаев.

15. Uppaal - системы со временем. Назначение и свойства Uppaal. Описание автоматов.

Моделирование системы. Верификация. Документирование и рассмотрение отдельных случаев.

16. Kronos - временной Model-checking. Назначение и свойства Kronos’а. Описание автоматов. Синхронизированное произведение. Model-checking. Документирование и рассмотрение отдельных случаев.

17. HyTech - линейные гибридные системы. Назначение и особенности HyTech. Описание автоматов. Анализ системы и анализ параметров. Документирование и рассмотрение отдельных случаев.

7. Учебно-методическое и информационное обеспечение дисциплины а) основная литература:

1. Алексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. – Ярославль: ЯрГУ, 2004.

2. Кузьмин Е.В. Верификация моделей программ. – Учебное пособие, Ярославль, ЯрГУ, 2008. – 176 с.

3. Кузьмин Е.В. Введение в теорию вычислительных процессов и структур. – Учебное пособие, Ярославль, ЯрГУ, 2006. – 140 с.

б) дополнительная литература:

1. Грис Д. Наука программирования. – М.: Мир, 1984. – 416 с.

2. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. – 560 с.

3. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. – М.: МЦНМО, 2002. – 416 с.

4. Карпов Ю. Г. Теория автоматов. – СПб.: Питер, 2003. – 208 с.

5. Математическая логика в программировании: сб. статей 1980—1988 гг.: Пер. с англ. – М.: Мир, 1991. – 408 c.

6. Минский М. Вычисления и автоматы – М.: Мир, 1971. – 268 c.

7. Непомнящий В.А., Рякин М.О. Прикладные методы верификации программ – М.:

Радио и связь, 1988. – 256 с.

8. Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984. – 9. Хоар Ч. Взаимодействующие последовательные процессы. – М.: Мир, 1989. – 264 с.

10. Хопкрофт Д., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений. – М.: Вильямс, 2002. – 528 с.

в) программное обеспечение и Интернет-ресурсы:

1. SMV. Symbolic Model Verifier. Carnegie Mellon University.

http://www.cs.cmu.edu/~modelcheck/smv.html 2. SPIN. http://spinroot.com/spin/whatispin.html 3. UPPAAL. http://www.uppaal.com 8. Материально-техническое обеспечение дисциплины Компьютер, мультимедийный проектор, набор электронных презентаций и схем.

Программа составлена в соответствии с федеральными государственными требованиями к структуре основной профессиональной образовательной программы послевузовского профессионального образования (аспирантура) (приказ Минобрнауки от 16.03.2011 г. № 1365) с учетом рекомендаций, изложенных в письме Минобрнауки от 22.06.2011 г. № ИБ – 733/12.

Программа одобрена на заседании кафедры теоретической информатики.

17.10.2012 г. (протокол № 11)