'

ДОКАЗАТЕЛЬНОЕ ПРОЕКТИРОВАНИЕ РЕАКТИВНЫХ АЛГОРИТМОВ

Понравилась презентация – покажи это...





Слайд 0

ДОКАЗАТЕЛЬНОЕ ПРОЕКТИРОВАНИЕ РЕАКТИВНЫХ АЛГОРИТМОВ Чеботарев Анатолий Николаевич Институт кибернетики им.В.М.Глушкова НАН Украины ancheb@gmail.com Семинар «Образный компьютер» 24.05.2011


Слайд 1

РЕАКТИВНЫЕ СИСТЕМЫ Под реактивными системами понимаются системы, постоянно взаимодействующие со своим окружением. Примеры таких систем системы управления технологическими процессами, телекоммуникационные сети, системы управления летательными аппаратами и др. Функционирование таких систем состоит в выработке реакции на сигналы, поступающие из окружающей среды.


Слайд 2

ФУНКЦИОНАЛЬНАЯ МОДЕЛЬ РЕАКТИВНОГО АЛГОРИТМА


Слайд 3

ПОДХОД К ПРОЕКТИРОВАНИЮ При проектировании систем управления потенциально опасными объектами необходимо гарантировать точное соответствие алгоритма управления всем требованиям к функционированию системы. В основе подхода лежит спецификация функциональных требований к системе в языке логики предикатов и формальный переход от спецификации к процедурному представлению алгоритма функционирования проектируемой системы.


Слайд 4

ОСНОВНЫЕ ПОДХОДЫ К КОРРЕКТНОМУ ПРОЕКТИРОВАНИЮ РЕАКТИВНЫХ АЛГОРИТМОВ ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ доказывает, что полученный алгоритм обладает некоторыми свойствами, однако не гарантирует, что он в точности соответствует своему назначению.


Слайд 5

ОСНОВНЫЕ ПОДХОДЫ К КОРРЕКТНОМУ ПРОЕКТИРОВАНИЮ РЕАКТИВНЫХ АЛГОРИТМОВ СИНТЕЗ гарантирует точное соответствие между спецификацией требований к алгоритму и ее процедурной реализацией.


Слайд 6

ОСНОВНЫЕ ПОДХОДЫ К КОРРЕКТНОМУ ПРОЕКТИРОВАНИЮ РЕАКТИВНЫХ АЛГОРИТМОВ ДОКАЗАТЕЛЬНОЕ ПРОЕКТИРОВАНИЕ доказывается корректность всех процедур проектирования, а также всех преобразований, выполняемых разработчиком в процессе интерактивного проектирования.


Слайд 7

ЯЗЫКИ СПЕЦИФИКАЦИИ ? = {p1, …, pk} – ПРЕДИКАТНЫЕ СИМВОЛЫ t – ПЕРЕМЕННАЯ, СО ЗНАЧЕНИЯМИ ИЗ Z ВИД ФОРМУЛ СПЕЦИФИКАЦИИ : ?t F(t) ЯЗЫК L F(t) – ФОРМУЛА, ПОСТРОЕННАЯ С ПОМОЩЬЮ ЛОГИЧЕСКИХ СВЯЗОК ИЗ АТОМОВ ВИДА p(t + k), где p ? ?, k ? Z.


Слайд 8

ПРИМЕР СПЕЦИФИКАЦИИ


Слайд 9

{Y1(Y2) РАВЕН 1 ТОЛЬКО ТОГДА, КОГДА X1(X2) =1} Y1(t) ? X1(t) , Y2(t) ? X2(t), {СТАВ РАВНЫМ 1, Y1(Y2) СОХРАНЯЕТ ЭТО ЗНАЧЕНИЕ , ПОКА X1(X2) = 1} Y1(t–1) & X1(t) ? Y1(t), Y2(t–1) & X2(t) ? Y2(t), {ВЗАИМНОЕ ИСКЛЮЧЕНИЕ} ?(Y1(t) & Y2(t)), {Y1(Y2) ИЗМЕНЯЕТСЯ В 1 ОДНОВРЕМЕННО С X1(X2)} X1(t) ? (Y1(t) ? Y2(t)), X2(t) ? (Y1(t) ? Y2(t)). F = ?tF(t) ПРИМЕР СПЕЦИФИКАЦИИ


Слайд 10

ЯЗЫК L* ДОБАВЛЯЕТСЯ КОНСТРУКЦИЯ ?t1(t1? t+k1)&F1(t1)&?t2(t1+k2? t2? t+k3) ? F2(t2), F1(t1) – ФОРМУЛА ЯЗЫКА L*, F2(t2) – ФОРМУЛА ЯЗЫКА L, k1, k2, k3? Z.


Слайд 11

СВЕРХСЛОВА ПУСТЬ ?i ? ? (i ? Z) …?-2?-1?0?1?2… – ДВУСТОРОННЕЕ СВЕРХСЛОВО ( ?Z ) ?1?2… – СВЕРХСЛОВО ( ??) …?-2?-1 ?0 – ОБРАТНОЕ СВЕРХСЛОВО ( ?– ?) АЛФАВИТ ? = {<00…0>, …, <11...1>} ?* – МНОЖЕСТВО ВСЕХ СЛОВ В АЛФАВИТЕ ?


Слайд 12

СВЕРХСЛОВА ПУСТЬ k ? Z И u ? ?Z k-префикс u(– ?, k) = …?k–2?k–1?k k-суффикс u(k + 1, ?) = ?k+1?k+2…


Слайд 13

АВТОМАТЫ (X–Y) – АВТОМАТ A = ?X, Y, Q, ?A?, ГДЕ ?A: Q ? X ? Y? Q – ФУНКЦИЯ ПЕРЕХОДОВ, ? = X ? Y ?-АВТОМАТ A = ??, Q, ?A?, ГДЕ ?A: Q ? ? ? Q СВЕРХСЛОВА И АВТОМАТЫ. l = ?1??… ДОПУСТИМО В СОСТОЯНИИ q АВТОМАТА A, ЕСЛИ СУЩЕСТВУЕТ ТАКОЕ СВЕРХСЛОВО q0q1q2…,ГДЕ q0 = q, ЧТО ДЛЯ ЛЮБОГО i = 0, 1, 2,… ?A(qi, ?i+1) = qi+1.


Слайд 14

АВТОМАТЫ ПУСТЬ Q = {q1, …, qn} – МНОЖЕСТВО СОСТОЯНИЙ АВТОМАТА A. СЕМЕЙСТВО МНОЖЕСТВ (S1, …, Sn), ГДЕ Si – МНОЖЕСТВО ВСЕХ СВЕРХСЛОВ, ДОПУСТИМЫХ В СОСТОЯНИИ qi (i = 1, 2, …, n), НАЗЫВАЕТСЯ ПОВЕДЕНИЕМ АВТОМАТА A.


Слайд 15

ФОРМУЛЫ И АВТОМАТЫ ИНТЕРПРЕТАЦИЯ ЯЗЫКА ПУСТЬ ? = {p1, …, pk} p1 …0110100… . . . . ? = {<00…0>, …, <11...1>} pk …1001110… MF – МНОЖЕСТВО ВСЕХ МОДЕЛЕЙ ДЛЯ F, WF – МН – ВО ВСЕХ 0-СУФФИКСОВ ИЗ MF , u ? MF Su = { l ? ?? | u(– ?, 0)?l ? MF} ?F = {Su | u ? MF} = {S1, …, Sn}


Слайд 16

ФОРМУЛЫ И АВТОМАТЫ ФОРМУЛА F = ?tF(t) СПЕЦИФИЦИРУЕТ АВТОМАТ A, ПОВЕДЕНИЕ КОТОРОГО СОВПАДАЕТ С ?F = {S1, …, Sn} .


Слайд 17

ОСНОВНЫЕ ПРОЦЕДУРЫ ПРОЕКТИРОВАНИЯ ПРОВЕРКА НЕПРОТИВОРЕЧИВОСТИ ВЕРИФИКАЦИЯ СПЕЦИФИКАЦИИ ПРЕОБРАЗОВАНИЕ СПЕЦИФИКАЦИИ ВО МНОЖЕСТВО ДИЗЪЮНКТОВ ПОСТРОЕНИЕ АВТОМАТА, ПРЕДСТАВЛЕННОГО МНОЖЕСТВОМ СОСТОЯНИЙ И ФУНКЦИЯМИ ПЕРЕХОДОВ И ВЫХОДОВ ДЕТЕРМИНИЗАЦИЯ АВТОМАТА


Слайд 18

ОСОБЕННОСТИ ПОДХОДА ОГРАНИЧЕННЫЙ СИНТАКСИС ЯЗЫКА СПЕЦИФИКАЦИИ ИНТЕРПРЕТАЦИЯ ЯЗЫКА НА МНОЖЕСТВЕ ЦЕЛЫХ ЧИСЕЛ ИСПОЛЬЗОВАНИЕ МОДЕЛИ НЕИНИЦИАЛЬНОГО АВТОМАТА ДЛЯ ПРЕДСТАВЛЕНИЯ РЕАКТИВНОГО АЛГОРИТМА


Слайд 19

СПАСИБО ЗА ВНИМАНИЕ!


×

HTML:





Ссылка: