Современные проблемы информатикиЛекция 1ВведениеТранзиционные системы презентация

Содержание

План лекций Теория взаимодействующих процессов (CCS, CSP, ACP) Инсерционное программирование (агенты и среды) Темпоральная логика и проверка моделей (model checking) Верификация софтвера (MSC, SDL, UML) Пруверы и солверы

Слайд 1Современные проблемы информатики Лекция 1 Введение Транзиционные системы


Слайд 2План лекций
Теория взаимодействующих процессов (CCS, CSP, ACP)
Инсерционное программирование (агенты и

среды)
Темпоральная логика и проверка моделей (model checking)
Верификация софтвера (MSC, SDL, UML)
Пруверы и солверы

Слайд 3Теории взаимодействия и параллелизма (communication, interaction and concurrency)
Структурная теория автоматов
Сети Петри
CCS

=> π-calculus (R.Milner)
CSP (T.Hoar)
ACP (J.A.Bergstra, J.W.Klop) => Handbook on Process Algebra (2000)
Коалгебры (J.J.M.M.Rutten, TCS 249(2000))
Mobile ambients (L.Cardelli, A.Gordon)
Агенты и среды (инсерционное программирование)
(A.Letichevsky, D.Gilbert, 1999)

Слайд 4Транзиционные системы
Ординарные транзиционные (динамические) системы :
S – пространство состояний
Т – отношение

переходов

Транзитивное замыкание

Движение в фазовом пространстве (поток)

Изменение состояния электронной системы

Изменение состояния софтверной системы


Слайд 5D.Park (1981)
Размеченные транзиционные системы
А – множество меток
символы,

события,
действия

Автоматы:
входные символы, вход/выход

Программы:
операторы, условия

Исчисления:
состояния – формулы,
действия – правила вывода

Взаимодействующие распределенные системы:
передача (прием) сообщений

Базы данных
запросы, ответы


Слайд 6Смешанные системы
наблюдаемые переходы
скрытые переходы


Слайд 7Атрибутные транзиционные системы
D={0,1}

(Не размеченные переходы)
Автоматы Мура
Программы над памятью
Типизированная память
Системы Крипке (модальная

логика)

Слайд 8Настроенные системы
Другие важные классы транзиционных систем:
Стохастические и нечеткие;
Системы реального времени.

начальные состояния
заключительные состояния
неопределенные состояния

Слайд 9


Применения
Моделирование поведения и взаимодействия
Исследование моделей и предсказание
Спецификация
Верификация
Генерация кода
Генерация тестов
Софтвер
Хардвер
Экологические
Социальные

Средства исследования моделей


Доказательства

Моделирование

+

Системы

Биологические


Слайд 10Трассовая эквивалентность
История:
Трасса:
Трасса для атрибутной системы:
трассы из


Слайд 11Система детерминирована:




Слайд 13Бисимуляционная эквивалентность bisimilarity (Milner 1980, D.Park 1981)
Отношение бисимуляции (bisimulation):



Слайд 14Бисимуляция есть эквивалентность
Бисимуляционная эквивалентность состояний совпадает с максимальной бисимуляцией на S.


Слайд 15Отношение бисимуляции распространяется на
состояния разных систем.
Для детерминированных систем бисимуляционная


эквивалентность состояний совпадает с трассовой.

Бисимуляционная эквивалентность систем


Слайд 16Бисимуляционная эквивалентность смешанных систем


Слайд 17Редукция смешанных систем

Добавляем новые переходы и настройку состояний:



Удаляем скрытые переходы




Слайд 18Смешанная транзиционная система и ее редукция бисимуляционно эквивалентны
бисимуляция
смешанная система
ее редукция


Обратная связь

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

Email: Нажмите что бы посмотреть 

Что такое ThePresentation.ru?

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


Для правообладателей

Яндекс.Метрика