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

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

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

3 ФУНКЦИОНАЛЬНАЯ МОДЕЛЬ РЕАКТИВНОГО АЛГОРИТМА УПРАВЛЯЮЩАЯ ЧАСТЬ ВНЕШНЯЯ СРЕДА ОПЕРАЦИОННАЯ ЧАСТЬ

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

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

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

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

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

9 X2Y2 Y1 X1 ME t+1t-1t t+2 Y2 X1 Y1 X2 ПРИМЕР СПЕЦИФИКАЦИИ

10 { 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) ПРИМЕР СПЕЦИФИКАЦИИ

11 ЯЗЫК L* ДОБАВЛЯЕТСЯ КОНСТРУКЦИЯ t 1 (t 1 t + k 1 )&F 1 (t 1 )& t 2 (t 1 + k 2 t 2 t + k 3 ) F 2 (t 2 ), F 1 (t 1 ) – ФОРМУЛА ЯЗЫКА L*, F 2 (t 2 ) – ФОРМУЛА ЯЗЫКА L, k 1, k 2, k 3 Z. F1(t1)F1(t1) F2(t2)F2(t2) F(t)F(t) t1t1 t2t2 t

12 СВЕРХСЛОВА ПУСТЬ i (i Z) … … – ДВУСТОРОННЕЕ СВЕРХСЛОВО ( Z ) 1 2 … – СВЕРХСЛОВО ( ) … – ОБРАТНОЕ СВЕРХСЛОВО ( – ) АЛФАВИТ = {, …, } * – МНОЖЕСТВО ВСЕХ СЛОВ В АЛФАВИТЕ

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

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

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

16 ФОРМУЛЫ И АВТОМАТЫ ИНТЕРПРЕТАЦИЯ ЯЗЫКА ПУСТЬ = {p 1, …, p k } p 1 … …... = {, …, } p k … … M F – МНОЖЕСТВО ВСЕХ МОДЕЛЕЙ ДЛЯ F, W F – МН – ВО ВСЕХ 0-СУФФИКСОВ ИЗ M F, u M F S u = { l | u(–, 0) l M F } F = {S u | u M F } = {S 1, …, S n }

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

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

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

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