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

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

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

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

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

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

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

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

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

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

ЯЗЫК 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

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

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

АВТОМАТЫ (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.

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

ФОРМУЛЫ И АВТОМАТЫ ИНТЕРПРЕТАЦИЯ ЯЗЫКА ПУСТЬ = {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 }

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

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

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

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