Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик

Нажмите для полного просмотра!

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №2

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №3

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №4

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №5

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №6

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №7

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №8

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №9

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №10

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №11

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №12

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №13

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №14

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №15

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №16

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №17

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №18

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №19

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №20

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №21

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №22

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №23

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №24

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №25

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №26

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №27

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №28

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №29

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №30

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №31

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №32

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №33

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №34

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №35

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механик, слайд №36

Содержание ▲

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

Слайды и текст этой презентации

Слайд 1

Описание слайда:

Автоматное программирование А.А. Шалыто Санкт-Петербургский государственный университет информационных технологий, механики и оптики 2007 г.

Слайд 2

Описание слайда:

Автоматное программирование Предложено мною в 1991 году Программные системы предлагается разрабатывать так же, как выполняется автоматизация технологических (и не только) процессов Система управления является системой взаимодействующих конечных автоматов

Слайд 3

Описание слайда:

Автоматное программирование

Слайд 4

Описание слайда:

Как строить программы?

Слайд 5

Описание слайда:

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

Слайд 6

Описание слайда:

Применение «Железо» Микропроцессоры Микроконтроллеры Программируемые логические контроллеры Парадигмы Процедурная Объектно-ориентированная Языки контроллеров Лестничные схемы Функциональные схемы

Слайд 7

Описание слайда:

Инструментальное средство UniMod (1) Инструментальное средство для поддержки автоматного программирования Создано в рамках ФЦНТП «Исследования и разработки по приоритетным направлениям развития науки и техники» на 2002-2006 годы по приоритетному направлению «Информационно-телекоммуникационные системы» Критическая технология – «Технология производства программного обеспечения» Вошел в число 15 наиболее инновационно перспективных и социально значимых проектов Федерального агентства по науке и инновациям

Слайд 8

Описание слайда:

Инструментальное средство UniMod (2) Локальная и удаленная отладка диаграмм в терминах состояний Проверка формальных свойств диаграмм Интерпретируемый и компилируемый подходы Запись автоматов в нотации UML-диаграмм классов и состояний Встраиваемый редактор UML-диаграмм для платформы Eclipse Запуск диаграмм в «одно нажатие»

Слайд 9

Описание слайда:

Инструментальное средство UniMod (3) Семь автоматов Вручную Автоматическая генерация Вручную

Слайд 10

Описание слайда:

Инструментальное средство UniMod (4) Один из автоматов – AL

Слайд 11

Описание слайда:

Движение за открытую проектную документацию Три задачи: Повышается качество обучения – обучение на проектах Создаются предпосылки для научной работы и отбор «ученых» Совершенствуется технология автоматного программирования Создано более 100 студенческих проектов, содержащих не только программную часть, но и открытую проектную документацию Из них – 15 UniMod-проектов Проекты опубликованы на сайте http://is.ifmo.ru

Слайд 12

Описание слайда:

Примеры. Игра «Космонавт» (1)

Слайд 13

Описание слайда:

Примеры. Игра «Космонавт» (2)

Слайд 14

Описание слайда:

Примеры. Игра «Космонавт» (3)

Слайд 15

Описание слайда:

Примеры. Игра «Космонавт» (4)

Слайд 16

Описание слайда:

Примеры. Игра «Lines» (1)

Слайд 17

Описание слайда:

Примеры. Игра «Lines» (2)

Слайд 18

Описание слайда:

Новые направления в автоматном программировании В рамках Федеральной целевой программы «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007–2012 годы» Технология генетического программирования для генерации автоматов управления системами со сложным поведением (шифр «2007-4-1.4-18-01-033») Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода (шифр «2007-4-1.4-18-02-041)

Слайд 19

Описание слайда:

Генерация автоматов и генетическое программирование Основная сложность в автоматном программировании – построение автоматов В большинстве случаев автоматы проектируются вручную Однако эвристическое построение автоматов часто затруднено или невозможно Решение – автоматическое построение конечных автоматов с помощью генетического программирования Это позволит повысить уровень автоматизации построения программ рассматриваемого класса Материалы – на сайте http://is.ifmo.ru (раздел «Генетические алгоритмы»)

Слайд 20

Описание слайда:

Три рассматриваемые задачи «Простая» задача – задача об «Умном муравье» «Сложная» задача – задача «Беспилотные летательные объекты» «Народная» задача – «Разливочная линия»

Слайд 21

Описание слайда:

«Простая» задача – задача об «Умном муравье» Тор – 32x32 89 клеток с едой 200 ходов Расположение еды и начальная позиция муравья фиксированы Цель – создать муравья, который съест всю еду Муравей = конечный автомат

Слайд 22

Описание слайда:

Эвристическое построение задачу не решает Пять состояний, за 200 ходов съедается 81 единица еды или все 89 единиц еды за 314 ходов

Слайд 23

Описание слайда:

Решение «простой» задачи Известные подходы – кодирование битовыми строками + генетический алгоритм Известные решения: 13 состояний (1992) 11 состояний (1993) 8 состояний (1999) Предлагаемый подход – генетическое программирование Построены два автомата с 7 состояниями после генерации 160 и 250 млн. автоматов Полный перебор ~3·1018 автоматов

Слайд 24

Описание слайда:

«Сложная» задача – задача «Беспилотные летательные объекты» Соревнование на дальность полета Две команды по восемь объектов Ограничения: запас топлива, столкновения, аэродинамическое взаимодействие Цель – разработка управляющей программы Задача заочного тура VI Открытой Всесибирской олимпиады по программированию (2005 год) Была решена при участии автора путем эвристического построения автоматов http://is.ifmo.ru/unimod-projects/plates/

Слайд 25

Описание слайда:

Решение (1) Система управления = нейронная сеть + конечный автомат Нейронная сеть преобразует вещественные входные переменные в логические

Слайд 26

Описание слайда:

Решение (2) Особь = две системы управления беспилотным объектом Особь из двух систем – для учета взаимодействия объектов

Слайд 27

Описание слайда:

Решение (3) Мутация особи Мутация системы управления летательным объектом Мутация нейронной сети Мутация элемента сети Мутация конечного автомата Изменение начального состояния Мутация перехода Скрещивание особей Скрещивание систем управления летающей тарелкой Скрещивание автоматов Скрещивание нейронных сетей

Слайд 28

Описание слайда:

Результаты применения генетического программирования За сутки была построена управляющая система, содержащая нейронную сеть и один автомат с шестью состояниями (вместо семи автоматов с 21 состоянием)

Слайд 29

Описание слайда:

Слайд 30

Описание слайда:

Решения «народной» задачи Построен вручную Построен автоматически

Слайд 31

Описание слайда:

Три традиционных подхода к верификации программ Тестирование – ничего не доказывает Доказательства теорем – все доказывает, но практически нигде не используется Верификация на моделях – Model Checking (модель программы с конечным числом состояний и свойства программы в темпоральной логике)

Слайд 32

Описание слайда:

Недостатки Model Checking для программ общего вида Не ясно, как построить модель Не ясно, как записать темпоральные свойства Не ясно, как перейти от модели к реальной программе в случае обнаружения ошибки

Слайд 33

Описание слайда:

Верификация автоматных программ Так как поведение автоматных программ задается графами переходов конечных автоматов, то все три указанные проблемы для этого класса программ эффективно решаются Работы проводятся совместно с кафедрой «Теоретическая информатика» Ярославского государственного университета им. П.Г. Демидова Материалы – на сайте http://is.ifmo.ru (раздел «Верификация»)

Слайд 34

Описание слайда:

Повышение качества программного обеспечения NASA (Открытые системы #03/2004) Использование состояний Генерация программ с помощью инструментального средства Stateflow Верификатор SPIN СПбГУ ИТМО http://is.ifmo.ru Использование состояний Генерация программ с помощью инструментального средства UniMod Верификаторы SPIN и Bogor

Слайд 35

Описание слайда:

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