Доказове проектування алгоритмів функціонування реактивних систем

Побудова нормальної форми для t-формули F(t) здійснюється у три етапи:

1) представлення F(t) у вигляді

Fi(t-1) & fi(t)

де Fi(t-1) - (-1)-обмежена формула, а fi(t) - елементарна формула, яка побудована з атомарних формул вигляду p(t);

2) представлення F(t) у вигляді (4.1), де Fi(t-1) (i = 1, …, n) - такі (-1)-обмежені формули, що при i № j Fi(t-1) & Fj(t-1) є 0 (умова ортогональності);

3) представлення F(t) у вигляді (4.1), що задовольняє усі вищенаведені вимоги і, додатково, умову: для усіх i, j = 1, 2, ..., n Fi(t-1) & fi(t) & Fj(t) Ы Fi(t-1) & fўi(t), де fўi(t) - формула такого ж вигляду, що і fi(t), причому fi(t) & fўi(t) Ы fўi(t).

Легко бачити, що результатом третього етапу є нормальна форма для формули F(t).

У дисертації показано, як формулу F(t) можна перетворити у еквівалентну їй формулу вигляду (4.1).

Перед тим, як перейти до другого етапу, для кожної максимальної $-підформули вводиться позначення вигляду ji(t-1) (i = 1, ..., s), де s - кількість максимальних $-підформул у перетвореній формулі, а ji - символи, що не зустрічаються у ній. Подальші еквівалентні перетворення будуть застосовуватися до формули, одержаної шляхом заміни усіх максимальних $-підформул їхніми позначеннями. Така формула трактуватиметься як скорочений запис для початкової формули.

До вигляду, який задовольняє умову ортогональності, формула перетворюється шляхом послідовного застосування співвідношення Fi(t-1) & fi(t) Ъ Fj(t-1) & & fj(t) Ы Fi(t-1) & ШFj(t-1) & fi(t) Ъ ШFi(t-1) & Fj(t-1) & fj(t) Ъ Fi(t-1) & Fj(t-1) & & (fi(t) Ъ fj(t)) до тих пар кон'юнктивних членів формули, які не задовольняють цю умову. Для обгрунтування останнього перетворення, яке дає нормальну форму, знадобиться наступна лема.

Лема 4.1. Нехай F(t) представлена у вигляді Fi(t-1) & fi(t), де Fi(t-1) - (-1)-обмежена формула, а fi(t) - елементарна формула, побудована з атомарних формул вигляду p(t) (i = 1, ..., n). Тоді множина моделей для формули F = "tFi(t) містить у собі множину моделей для формули "tF(t).

Наслідок.

"tF(t) Ы "tF(t) & (Fi(t))

Нормальна форма будується шляхом "розщеплення" підформул Fi(t-1) & fi(t), тобто представлення їх у вигляді диз'юнкції підформул аналогічного вигляду. Таке розщеплення здійснюється шляхом множення підформули Fi(t-1) & fi(t) на кожну Fj(t) (j = 1, ..., n). При цьому кожне входження $-підформули (її позначення) в Fj(t) замінюється еквівалентним йому виразом відповідно до рівносильності

F(t-1) & F2(t-k3) Ъ F1(t-k1) Ъ …Ъ F1(t-k2-k3+1), якщо k1 < k2 + k3,

F1(t-k1) & F2(t-k1) & … & F2(t+k2-k1), якщо k1 і k2 + k3.

Застосування цієї рівносильності може призвести до появи нових максимальних $-підформул і додаткових позначень для них. Якщо добуток Fi(t-1) & fi(t) & Fj(t) не дорівнює тотожно нулю, то він подається у формі, яка задовольняє умову ортогональності. Як випливає із леми 4.1, у результаті такого перетворення одержуємо формулу, еквівалентну початковій. Наведене перетворення повторюється доти, доки на черговому циклі перетворення кожний добуток Fi(t-1) & fi(t) & Fj(t) для усіх i й j не буде або рівним тотожно нулю, або мати вигляд Fi(t-1) & fўi(t).

Для того, щоб одержана нормальна форма задовольняла умову 4) теореми про специфікацію, достатньо на вигляд підформул Fi(t-1) у представленні (4.1) накласти обмеження, яке полягає у тому, що кожна така підформула є кон'юнкцією простих формул або їхніх заперечень.

Як правило, процедура синтезу застосовується до специфікацій у мові L, задля чого початкова специфікація, подана у мові L*, транслюється у мову L.

Формулу f(t) мови L одержуємо з формули F(t) мови L* шляхом заміни всіх $-підформул, які зустрічаються в ній, їх рекурсивними визначеннями згідно з рівносильністю (4.2).При цьому всі максимальні $-підформули замінюються позначеннями вигляду zi(t), з кожним із яких асоціюється формула zi(t) “ Qi(t), де Qi(t) відповідає правій частині рівносильності (4.2). Якщо Qi(t) містить $-підформули, то з ними вчиняють так само, як і з $-підформулами початкової формули. У результаті одержуємо множину E формул вигляду zi(t) “ Qi(t), у правих частинах яких відсутні $-підформули. Формула f(t) є кон'юнкцією перетвореної наведеним способом формули F(t) й усіх формул із E. Якщо zi у введених позначеннях розглядати як предикатні символи, то формула f(t) буде формулою мови L.

Вищеописаний метод синтезу автомата за специфікацією у мові L* адаптований для специфікації у мові L. Оскільки в основі методу лежить поняття нормальної форми формули F(t), уточнимо це поняття для формул вигляду F(t) мови L.

Нехай формула F(t) подана у вигляді

Fi(t-1) & fi(t)

де Fi(t-1) - формула, максимальний ранг атомів якої не перевищує -1, а fi(t) - формула, побудована з атомів рангу 0. Представлення F(t) у такому вигляді назвемо диз'юнктивним представленням, а кон'юнкцію вигляду Fi(t-1) & fi(t) - компонентом такого представлення з лівою частиною Fi(t-1) і правою частиною fi(t). Диз'юнктивне представлення задовольняє умову ортогональності, якщо для i № j (i, j О {1, …, n}) Fi(t-1) & Fj(t-1) є 0. Диз'юнктивне представлення формули F(t), яке задовольняє умову ортогональності, називається нормальною формою, якщо для кожного i = 1, …, n знайдеться таке j О {1, …, n}, що Fi(t-1) & fi(t) & Fj(t) Ы Fi(t-1) & fij(t), де fij(t) - несуперечна формула, побудована з атомів нульового рангу.

Нехай W = {p1, …, pq} - множина всіх предикатних символів, які зустрічаються в F(t), а S(W) - множина всіх двійкових векторів довжини q. Як було вище зазначено, символу s О S(W) відповідає елементарна кон'юнкція s?(t) вигляду p?1(t)& … & p?q(t), де p?j О {pj, Шpj}.

Специфікації F = "tF(t), де F(t) представлена в нормальній формі вигляду (4.3), відповідає S-автомат Aў(F) з вхідним алфавітом S(W), станами q1, …, qn і функцією переходів dў. Для s О S(W) і qi, qj О { q1, …, qn} dў(qi, s) = qj тоді й тільки тоді, коли Fi(t-1) & fi(t) & s?(t) & Fj(t) = Fi(t-1) & s?(t). Автомат A(F), який задовольняє специфікацію F, є максимальним циклічним підавтоматом автомата Aў(F). Побудова автомата A(F) складається з двох основних етапів: 1) побудови диз'юнктивного представлення формули F(t), яке задовольняє умову ортогональності; 2) побудови нормальної форми формули F(t). На першому етапі використовується те саме співвідношення, що і в загальному методі. На другому етапі для одержання нормальної форми формули F(t) здійснюється розщеплення компонентів її диз'юнктивного представлення шляхом множення їх на Fi(t). Для того, щоб число станів автомата A(F) було близьким до мінімального, на диз'юнктивне представлення F(t) вигляду (4.3), одержане перед початком процесу розщеплення компонент, накладається додаткова умова: для i № j (i, j О {1, …, n}) fi(t) не еквівалентна fj(t).

Для формул глибини Ј 1 процедура синтезу суттєво спрощується, оскільки в цьому випадку розщеплення компонент диз'юнктивного представлення формули F(t) відсутнє і алгоритм зводиться до побудови представлення, яке задовольняє умову ортогональності. У зв'язку з цим зазначимо, що будь-яку формулу мови L можна перетворити в формулу глибини Ј 1 шляхом введення додаткових предикатних символів.

Вищерозглянуті методи синтезу орієнтовані в основному на диз'юнктивне представлення специфікації і синтезують неініціальний автомат. Але зазвичай специфікація є кон'юнкцією великої кількості формул і синтезований неініціальний автомат може мати значно більше станів, ніж його ініціальний підавтомат. Крім того, багато перетворень, які здійснюються в процесі проектування алгоритму, розраховані на представлення специфікації у вигляді множини диз'юнктів. Тому бажано мати метод синтезу для будь-якого представлення специфікації, який може відразу будувати ініціальний автомат. Таким методом є запропонований метод індуктивної побудови автомата відповідно до структури формули F(t). У цьому методі елементарні кроки синтезу відповідають логічним операціям, які застосовуються при побудові формули F(t). Виходячи з нормальних форм для елементарних кон'юнкцій і диз'юнкцій, послідовно будується нормальна форма всієї специфікації.

Нормальна форма вигляду (4.3) задається множиною рядків [Fi(t)](fi(t)). Ліва частина рядка (взята у квадратні дужки) називається позначкою стану, а права - областю переходів. Над такими представленнями нормальних форм визначені операції диз'юнктивного добутку (відповідає диз'юнкції), кон'юнктивного добутку (відповідає кон'юнкції), заперечення і т.д.

При синтезі ініціального автомата деякі рядки нормальних форм виділяються як початкові, для чого використовується початкова умова. При виконанні операцій кон'юнктивного і диз'юнктивного множення ініціальних нормальних форм суттєве значення має послідовність множення рядків.

У п'ятому розділі розглянуто проблему, яка виникає при проектуванні відкритих систем і полягає у тому, щоб спроектувати автомат, який би функціонував відповідно до його специфікації при будь-якій допустимій поведінці зовнішнього середовища. Цю проблему сформульовано в термінах поняття узгодженості автомата із середовищем. Одержано теоретичні результати, які дозволяють будувати ефективні алгоритми аналізу узгодженості для автоматів зі скінченною пам'яттю, а також побудовано алгоритм розв'язання цієї задачі на рівні специфікацій автомата і середовища.

Відповідно до автоматної семантики специфікації реактивної системи дослідження її взаємодії з середовищем зводиться до розгляду взаємодії двох автоматів. Автомати, що взаємодіють (один з яких моделює поведінку керуючої частини алгоритму, що розробляється, а другий - поведінку середовища), утворюють структуру, в якій входи і виходи одного з автоматів з'єднані відповідно з виходами й входами другого. На можливу поведінку такої структури суттєво впливає частковість одного чи обох автоматів. У разі частковості автоматів, що взаємодіють, виникає проблема забезпечення правильності їхнього спільного функціонування, тобто виключення ситуації, коли в процесі функціонування автоматів перехід в одному з них під дією вхідного сигналу, який поступає від другого, не визначено. Відповідну задачу, яка виникає при проектуванні реактивних систем, можна сформулювати так: використовуючи інформацію про середовище, спроектувати систему так, щоб її спільне функціонування з середовищем було правильним.

У дисертації для уточнення і формалізації поняття правильної взаємодії автоматів введено поняття узгодженості автоматів. Узгодженість визначається як властивість циклічної композиції автоматів, яка задає спосіб їхньої взаємодії.

Специфікація автомата, що проектується, визначає клас автоматів, і задачею проектування є побудова автомата, який належить цьому класу. Інформація про середовище обмежує вибір представника з цього класу вимогою його узгодженості з середовищем. Тому аналіз узгодженості автоматів повинен не тільки давати відповідь на питання, чи узгоджені автомати, але й виділяти з множини всіх автоматів, які задовольняють специфікацію, підмножину автоматів, узгоджених з середовищем.

При формалізації проблеми узгодженості автоматів розглядаються часткові недетерміновані X-Y-автомати Мура. Якщо |X| = 1, то автомат А називається автономним Y-автоматом, який визначається четвіркою <Y, Q, cA, mA>. Функція переходів такого автомата має вигляд cA: Q ® 2Q. Для автономного Y-автомата розглядаються допустимі Y-слова і надслова.

Нехай A = <X, Y, QA, cA, mA> і B = <Y, X, QB, cB, mB> - часткові недетерміновані відповідно X-Y- і Y-X-автомати Мура.

Визначення 5.1. Симетрична циклічна композиція автоматів А і В є автономним недетермінованим Z-автоматом Мура С = <Z, QC, cC, mC>, де Z = XґY И YґX, QC = QAґQB И QBґQA, а функція переходів cC і функція виходів mC визначаються наступним способом. Для усіх q О QA і s О QB

cC(q, s) = {(s, q1) | q1 О cA(q, mB(s))},

cC(s, q) = {(q, s1) | s1 О cB(s, mA(q))},

mC(q, s) = (mA(q), mB(s)), mC(s, q) = (mB(s), m A(q)).

Визначення 5.2. Два циклічних часткових детермінованих X-Y- і Y-X-автомата Мура називаються узгодженими, якщо їх симетрична циклічна композиція має циклічний підавтомат.

Поняття узгодженості недетермінованих автоматів пов'язане з поняттям циклічної детермінізації недетермінованого автомата.

Визначення 5.3. Частковий недетермінований циклічний X-Y-автомат Мура А узгоджений з частковим недетермінованим циклічним Y-X-автоматом Мура В, якщо існує циклічна детермінізація автомата А, узгоджена з кожною циклічною детермінізацією автомата В.

Це визначення не конструктивне через нескінченність множини детермінізацій недетермінованого автомата. Щоб розробити практичні методи перевірки узгодженості автоматів введене поняття паралельної циклічної композиції.

Визначення 5.4. Паралельна циклічна композиція автоматів А = <X, Y, QA, cA, mA> і В = <Y, X, QB, cB, mB> є автономним недетермінованим Z-автоматом С = <Z, QC, cC, mC>, де Z = Y ґ X, QC = QB ґ QA, а функція переходів cC і функція виходів mC визначаються у такий спосіб: для будь-яких q, qў О QA і s, sў О QB (sў. qў) ОcC(s, q) тоді й тільки тоді, коли qў О cA(q, mB(sў)), sў О cB(s, mA(qў)); mC(s, q) = (mB(s), mA(q)).

При використанні паралельної циклічної композиції для перевірки узгодженості автомата А з автоматом В замість автомата В треба розглядати його так званий лівий зсув за входом (позначається B?). Якщо автомат В заданий множиною диз'юнктів CB, то множину диз'юнктів C?B, що специфікує автомат B?, одержуємо в результаті зменшення в диз'юнктах із CB рангу усіх W-літер (які визначають алфавіт Y) на 1.

Твердження 5.1. Частковий недетермінований циклічний автомат А узгоджений з частковим недетермінованим циклічним автоматом В тоді й тільки тоді, коли паралельна циклічна композиція D автоматів A і B? = <Y, X, Q?B, c?B, m?B> має циклічний підавтомат Dў = <Z, QўD, cD, mD>, для усякого стану (s, q) якого виконується наступна умова: для кожного sj О c?B(s) (тут і далі c?B(s) = ) існує таке (s1, q1) О cD(s, q) З QўD, що m?B(s1) = m?B(sj).

Таким чином, перевірка узгодженості автомата А з автоматом В полягає у з'ясуванні, чи має паралельна циклічна композиція D автоматів А і B циклічний підавтомат Dў з властивістю, описаною у твердженні 5.1. Це можна зробити шляхом послідовного видалення з паралельної циклічної композиції станів, які явно не належать підавтомату Dў.

Розглянемо особливості такого підходу, пов'язані із специфікацією автоматів А і B у вигляді множин диз'юнктів CA і C?B відповідно. У випадку, коли специфікація автомата задана множиною диз'юнктів C, відповідні автомати у просторі станів Q(r, W) позначимо Aў(r, C) і A(r, C). Оскільки множина W предикатних символів у диз'юнктах з CA і C?B одна й та сама, то вважаючи її однаково упорядкованою для обох специфікацій, як представників класів автоматів, що специфікуються, будемо розглядати автомати A = A(r, CA) і B? = A(r, C?B), побудовані в одному й тому ж просторі станів, глибина r якого дорівнює максимальній глибині диз'юнктів, що належать CA і C?B. Якщо стан (s, q) належить циклічному підавтомату паралельної циклічної композиції автоматів А і B, то станам s і q відповідає один і той же стан простору станів, що розглядається. Таким чином, замість паралельної циклічної композиції автоматів А і B можна розглядати автономний автомат A*, множина станів якого співпадає з перетином множин станів автоматів А і B, а функція переходів визначається виразом cA*(q) = cA(q) З c?B(q), де cA(q) = . При цьому умова вилучення стану набуває такого вигляду: стан q вилучається, якщо для нього існує така область переходу j = N(q, x), що F?B(t) істинна на j, а формула F*A(t) = = FA(t) & F?B(t), яка відповідає множині диз'юнктів C*A = CA И C?B, на цій області хибна. Остання умова відповідає тому, що cAў(q, x) = Ж. Зазначимо, що умова вилучення стану не зміниться, якщо до множини CA додавати не усі диз'юнкти з C?B, а тільки ті, які містять W-літери нульового рангу. Назвемо такі диз'юнкти диз'юнктами першого роду, а диз'юнкти, які не містять W-літер нульового рангу, - диз'юнктами другого роду.

Отже, перевірка узгодженості автомата А з автоматом В складається з двох етапів. На першому етапі шляхом послідовного вилучення станів будується підавтомат автомата Aў= Aў(r, CA И C?B), який не містить станів, що задовольняють вищесформульовану умову вилучення. Зазначені перетворення виконуються над множиною диз'юнктів CўA, яку одержуємо шляхом додавання до CA всіх диз'юнктів першого роду, що містяться в C?B, оскільки множини станів, які підлягають вилученню, для автоматів Aў і Aў(r, CўA) співпадають. На другому етапі одержана множина диз'юнктів перевіряється на несуперечність. Для цього використовується один із методів резолюцій. Зокрема, тут зручно застосовувати метод роздільного резольвування.

У шостому розділі розглянуто основні задачі, які виникають при верифікації реактивних алгоритмів методом перевірки здійсненності формули на моделі. Зокрема, одержано ефективне рішення таких задач, як побудова автомата-розпізнавача за формулою лінійної темпоральної логіки та редукція автоматної моделі алгоритму, що верифікується, тобто побудова такої моделі, яка еквівалентна вихідній відносно властивості, що перевіряється, але має суттєво меншу кількість станів.

Під верифікацією реактивного алгоритму розуміємо автоматичну перевірку наявності в нього певних властивостей. Різновид верифікації, яку запропоновано в дисертації, відноситься до категорії перевірки істинності формули при заданій інтерпретації. У таких методах моделлю системи, що верифікується, є частковий недетермінований автомат А, а властивість, що перевіряється, задається у вигляді темпоральної формули j. Теоретико-автоматний підхід до верифікації полягає в тому, що за запереченням формули j будується автомат-розпізнавач AШj, який представляє (розпізнає) ту саму w-мову, що й Шj. Перевірка здійсненності формули j зводиться до перевірки непустоти w-мови, яка розпізнається прямим добутком автомата AШj і автомата A. Складність розв'язання останньої задачі лінійно залежить від складності (кількості станів) автоматної моделі алгоритму, що верифікується, і автомата AШj.. Тому велике значення має проблема зменшення кількості станів цих автоматів.

У порівнянні зі стандартним варіантом мови LTL запропонована мова темпоральної логіки з лінійним часом має дві відміни. Перша з них полягає в тому, що атомами, з яких за допомогою логічних зв'язок і темпоральних операторів будуються формули, є не пропозиційні змінні, як це має місце в LTL, а елементи довільної бульової алгебри. Зокрема, ними можуть бути будь-які пропозиційні формули від двійкових змінних. Друга відміна полягає в тому, що замість темпорального оператора Xj (наступного моменту j істинна) використовується більш загальний оператор <t>j, який набуває істинного значення тоді й тільки тоді, коли в нинішній момент істинною є пропозиційна формула t, а наступного моменту - темпоральна формула j. Така модифікація логіки LTL спрямована на зменшення кількості підформул у формулі специфікації, що спрощує алгоритм синтезу й зменшує кількість станів автомата, який ми отримуємо.

Нехай B - бульова алгебра з операціями Ъ, & та Ш. На елементах B визначимо відношення часткового порядку Ј : для a, b О B a Ј b тоді й тільки тоді, коли a & b = a. Множиною атомів бульової алгебри B називається множина A (B) усіх ненульових і мінімальних відносно Ј її елементів. Зокрема, якщо B - бульова алгебра всіх підмножин множини S, то A (B) = S, а якщо B - множина всіх бульових функцій від змінних {p1, …, pq}, то A (B) - множина всіх конституент одиниці від цих змінних. Як мову для задання властивостей будемо використовувати темпоральну логіку з лінійним часом над скінченною бульовою алгеброю B. Позначимо цю логіку LTL(B). Множина формул LTL(B) визначається наступним способом.

1. Символ true є формулою.

2. Якщо t О B, а f1 і f2 - формули, то формулами є також f1 Ъ f2, Шf1, <t>f1 і f1Uf2.

Додаткові формули вводяться як скорочення: f1&f2 = Ш(Шf1Ъ Шf2), Gf1 = Ш(true UШf1) і f1Wf2 = (f1Uf2) Ъ Gf1.

Формули LTL(B) інтерпретуються на надсловах над S = A (B).

Розглянемо представлення w-мови W(j), яка задається формулою j логіки LTL(B), за допомогою автомата-розпізнавача над алфавітом S = A (B).

Автомат (розпізнавач) A над алфавітом S визначається четвіркою об'єктів

A = <S, s0, d, Б>, де S - скінченна множина станів; s0 О S - початковий стан; d : S ґ ґ S ® 2S - функція переходів (недетермінована); Б Н 2S - сукупність множин станів (забороняючих множин).

w-слово в алфавіті S назвемо вхідним w-словом, а w-слово в алфавіті S - w-словом станів.

Реакцією автомата A на вхідне w-слово a = s0s1 ... називається кожне w-слово станів b = s0s1 ..., таке, що s0 - початковий стан і для усіх i і 0 si+1 О d(si, si). Реакція b називається допустимою тоді й тільки тоді, коли не існує такого i і 0, що усі sj (j і i) належать одній і тій самій множині із Б. Вхідне w-слово a розпізнається автоматом A тоді й тільки тоді, коли існує допустима реакція автомата A на це w-слово. Множина W(A) усіх w-слів, які розпізнаються автоматом A, називається w-мовою, що розпізнається цим автоматом.

Для побудови за формулою j автомата Aj такого, що W(Aj) = W(j), формула j подається у вигляді кореневого розміченого ациклічного графа Gj, вершинам якого відповідають оператори логіки LTL(B). Будь-яка вершина v в такому графі визначає підформулу формули j, подану у вигляді підграфа з коренем v. Кожна вершина графа Gj позначається індексом з деякої множини індексів. Індекс, яким позначається корінь графа Gj, називається початковим.

Розміченому графу Gj поставимо у відповідність автомат Aj = <S, s0, d, Б> над алфавітом S. Станами цього автомата є множини індексів, причому початковий стан s0 - це множина {i0}, яка складається з одного початкового індексу. Пустій множині індексів відповідає такий стан s*, що для будь-якого s О S d(s*, s) = s*. Множина станів S визначається в процесі побудови автомата як множина всіх станів, досяжних з початкового S стану. Кожний індекс, що позначає вершину графа Gj, яка відповідає оператору U, визначає одну й ту саму множину в сукупності Б забороняючих множин станів, а саме множину всіх тих станів із S, яка містить цей індекс. Таким чином, число забороняючих множин дорівнює числу вершин графа Gj, які відповідають оператору U. Значення функції переходів d(s, s), де s = {i1, ..., ik}, s О S, визначається в два етапи. Спочатку відповідно до описаних у дисертації правил виконується процедура заміни індексів, яка перетворює s у сукупність множин індексів {I1, ..., In}. Далі для кожної множини Ij О {I1, ..., In} обчислюється множина індексів, у яку Ij перетворюється вхідним символом s, що і визначає, врешті-решт, значення функції d(s, s).

Суттєвою особливістю запропонованого алгоритму є нове поняття стану автомата, що синтезується, а також здійснення поглинань на двох етапах обчислювання функції переходів. Це дозволило значно скоротити кількість станів і переходів у автоматі, що синтезується, у порівнянні з кращими із відомих методів.

У ряді випадків система, що верифікується, є композицією взаємодіючих між собою модулів. Кількість станів автоматної моделі такої системи росте експоненціально з числом модулів, з яких складається система. При кількості модулів у декілька десятків складність моделі, що верифікується, - одна з основних перешкод для застосування методів формальної верифікації. З іншого боку, властивість, що верифікується, у таких випадках можна задати у вигляді кон'юнкції формул, кожна з яких залежить від невеликої кількості змінних. Основна ідея запропонованого методу редукції полягає в тому, що для заданої множини V1 “локальних” змінних будується такий автомат A1, що будь-яка формула, яка залежить тільки від змінних з V1, істинна на w-словах, представлених автоматом A1, тоді й тільки тоді, коли вона істинна на w-словах, представлених автоматом A.

Нехай V - скінченна множина символів і V1 Н V. Позначимо B(V) бульову алгебру всіх бульових функцій від аргументів з V. Нехай S = A (B(V)), а S1 = A (B(V1)). Визначимо відображення

x: S ® S1 так, що x(s) = sў тоді й тільки тоді, коли s & sў = = sў. Відображення x поширимо на

w-слова й множини w-слів. Тепер вимоги до автомата A1 можна записати у вигляді наступних двох умов:

1) для кожного a О W(A) x(a) О W(A1),

2) для кожного aў О W(A1) існує таке a, що x(a) = aў.

Якщо A - автомат над алфавітом S = A (B(V)), то проекцією автомата A на V1 назвемо автомат A1 з тою самою множиною станів, що і A, функцію переходів якого одержуємо з функції переходів автомата A заміною кожного s О S на x(s). У загальному випадку автомат A1 буде недетермінованим. Легко бачити, що автомат A1 задовольняє умови 1), 2).

Побудова редукції автомата А для заданої множини V1 здійснюється у такий спосіб. Будується проекція автомата А на V1, потім одержаний автомат детермінізується, тобто будується еквівалентний йому детермінізований автомат, станами якого є підмножини множини станів автомата А, після чого до цього автомата застосовується процедура мінімізації кількості станів. Оскільки як детермінізація, так і мінімізація зберігають множину w-слів представлених автоматом, то збудована таким чином редукція автомата А також задовольнятиме умови 1) і 2).

Запропонована процедура редукції моделі, що верифікується, на відміну від багатьох евристичних методів, які потребують обов'язкової участі людини, може виконуватися цілком автоматично.

У сьомому розділі наведено опис двох експериментальних систем PROCOD і Dual. Обидві системи призначені для автоматизованого (або автоматичного) доказового проектування автоматів за логічною специфікацією у мові L. Система PROCOD функціонує в операційному середовищі MS DOS, а система Dual - у середовищі Windows. Вхідними даними для систем є специфікація автомата, що проектується, специфікація середовища та початкова умова. Кінцевим результатом роботи є процедурний опис автомата в текстовій і графічній формах. Кожне втручання проектувальника в процес проектування в системі PROCOD контролюється для того, щоб запобігти одержанню результату, що не задовольняє початкову специфікацію.

У додатках розглянуто приклади використання систем PROCOD і Dual для розв'язання задач проектування.

ВИСНОВКИ

Результатом дисертаційної роботи є розв'язання важливої прикладної проблеми забезпечення безпомилковості процесу проектування реактивних алгоритмів промислового рівня складності на етапі побудови процедурного представлення алгоритму. Для цього було побудовано теорію доказового проектування алгоритмів і на її основі розроблено методологію проектування, яка гарантує одержання процедурного представлення алгоритму, що задовольняє вимоги до його функціонування, сформульовані у початковій специфікації.

Головною перешкодою на шляху побудови теорії і методології автоматизованого проектування алгоритмів функціонування реактивних систем є надто велика обчислювальна складність розв'язання багатьох задач проектування. Ці задачі, зазвичай, належать до класів NP- і PSPACE-повних проблем, тому не можна розраховувати на одержання ефективних алгоритмів (що дозволяють розв'язувати практичні задачі на сучасних обчислювальних засобах) для розв'язання будь-яких задач проектування. Запропонований підхід до побудови теорії та засобів автоматизованого проектування реактивних систем полягає в розумному обмеженні класу задач, що розв'язуються, такими задачами, для яких можна отримати рішення з припустимими обчислювальними витратами. “Розумність” обмеження полягає в тому, щоб цей клас містив у собі практично важливі задачі, тобто задачі такого рівня складності, який відповідає складності сучасних реактивних систем. Природним способом обмеження класу задач є обмеження виражальних можливостей мови, на якій формулюється задача, у даному випадку - мови специфікації реактивних алгоритмів. Виражальні можливості мови, у свою чергу, визначаються її синтаксисом та семантикою.

Отже, основна ідея запропонованого підходу полягає в тому, щоб визначити такі обмеження на синтаксис та семантику мови специфікації, які б дозволили побудувати теоретично обгрунтовані формальні методи проектування реактивних алгоритмів промислового рівня складності.

В процесі вирішення зазначеної вище проблеми одержано такі основні теоретичні та практичні результати.

1. Запропоновано та теоретично обгрунтовано дворівневу організацію системи мов опису, основаних на логіці першого порядку з одномісними предикатами. Виражальні засоби мови нижнього рівня максимально обмежені так, щоб одержати ефективні методи розв'язку задач проектування для специфікацій у цій мові й водночас мати прості алгоритми трансляції в неї із значно виразнішої мови верхнього рівня. Використання для інтерпретації мов множини цілих чисел замість натуральних дозволило спростити побудову специфікації алгоритму, зробити її більш природною (формули описують вимоги до поведінки системи, виходячи з історії її функціонування) і, головне, суттєво поліпшити ефективність відповідних логічних методів розв'язку задач проектування.

2. Сформульовано й доведено теорему про специфікацію, яка визначає зв'язок між структурою певного представлення формули мови специфікації і процедурним (у термінах станів і функцій переходів і виходів) представленням автомата, який специфікується цією формулою. На основі цієї теореми запропоновано підхід до вибору мови верхнього рівня, який дозволяє використовувати теорему про специфікацію для побудови алгоритмів синтезу, суттєво простіших за алгоритми синтезу, які базуються на методі табло для мов темпоральних логік.

3. Розроблено та теоретично обгрунтовано методи перевірки несуперечності специфікацій на основі резолюційної процедури пошуку логічного виведення. Використання специфіки запропонованого методу інтерпретації мов і побудови їхньої семантики дозволило суттєво поліпшити ефективність методу резолюцій порівняно з традиційними його варіантами. Методи перевірки несуперечності специфікацій реалізовано у вигляді процедур R- і S-поповнення, які використовуються не тільки як засоби перевірки несуперечності, але й як складові багатьох процедур проектування.

4. Для сформульованої у дисертації проблеми детермінізації логічних специфікацій одержано математично обгрунтоване її рішення. Побудовано реалізацію одержаного методу детермінізації, яка дозволяє задавати різні способи детермінізації, що в загальному випадку приводять до різних реалізацій алгоритму, що проектується.

5. Для сформульованої у новій постановці проблеми забезпечення коректності взаємодії між системою, що проектується, і зовнішнім середовищем одержано ефективне рішення на основі теоретико-автоматних і логічних методів. Ефективність її рішення особливо важлива в методології доказового проектування, де ця проблема виникає при перевірці коректності перетворень, що виконуються неформально.

6. На основі теореми про специфікацію одержано ряд нових методів розв'язання задачі синтезу автомата за його логічною специфікацією. Уперше в рішенні практичної задачі синтезу використовувалися топологічні властивості мови специфікації, що дозволило сформулювати обмеження на виражальні можливості мови, які призвели до значного підвищення ефективності методів синтезу.

7. В області верифікації алгоритмів запропоновано метод синтезу автомата-розпізнавача за формулою лінійної темпоральної логіки, що відрізняється від відомих методів модифікованою моделлю автомата-розпізнавача та способом визначення поняття стану автомата, що синтезується. Це дозволило одержати значно кращі результати щодо кількості станів та переходів у автоматах, що синтезуються, порівняно з останніми із відомих методів. Запропоновано також метод редукції моделі системи, що верифікується, який дозволяє в багатьох випадках значно зменшити кількість станів. На відміну від евристичних методів, які звичайно використовуються і потребують побудови редукції методом послідовних проб, або методів редукції на основі гомоморфізму, які не завжди можна застосувати, запропонований метод може виконуватися цілком автоматично і завжди дає результат, еквівалентний початковій моделі відносно властивостей, що перевіряються.

Усі запропоновані в дисертації методи розв'язання задач проектування базуються на строго доведених теоретичних результатах, багато з яких сформульовано у вигляді теорем, що мають самостійне значення.

Основні положення дисертації опубліковані в таких працях:

1. Чеботарев А.Н. Взаимодействие автоматов // Кибернетика. - 1991. - N6. - C. 17-29.

2. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. I // Кибернетика и системный анализ. - 1993. - N3. - С. 31-42.

3. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. II. // Кибернетика и системный анализ. - 1993. - N4. - C. 3-14.

4. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем. III. // Кибернетика и системный анализ. - 1993. - N6. - C. 3-17.

5. Chebotarev A.N., Morokhovets M.K.. Consistency checking of automata functional specifications // Proc. LPAR'93, Lecture notes in Artificial Intelligence. - 1993. - V. 698. - P. 76-85.

6. Чеботарев А.Н. Проверка непротиворечивости простых спецификаций автоматных систем // Кибернетика и системный анализ. - 1994. - N3. - C. 3-11.

7. Мороховец М.К., Чеботарев А.Н. Резолюционный подход к проверке согласованности взаимодействующих автоматов // Кибернетика и системный анализ. - 1994. - N6. - C. 36-50.

8. Чеботарев А.Н. Детерминизация логических спецификаций автоматов // Кибернетика и системный анализ. - 1995. - N1. - C. 3-12

9. Чеботарев А.Н. Синтез недетерминированного автомата по его логической спецификации. I // Кибернетика и системный анализ. - 1995. - N5. - C. 3-15.

10. Чеботарев А.Н. Синтез недетерминированного автомата по его логической спецификации. II // Кибернетика и системный анализ. - 1995. - N6. - C. 16-26.

11. Чеботарев А.Н. Расширение логического языка спецификации автоматов и проблема синтеза // Кибернетика и системный анализ. - 1996. - N6. - C. 11-27.

12. Чеботарев А.Н. Синтез процедурного представления автомата, специфицированного в логическом языке L*. I // Кибернетика и системный анализ. - 1997. - N4. - C. 60-74.

13. Чеботарев А.Н. Синтез процедурного представления автомата, специфицированного в логическом языке L*. II // Кибернетика и системный анализ. - 1997. - N6. - C. 115-127.

14. Chebotarev A.N., Morokhovets M.K.. Resolution-based approach to compatibility analysis of interacting automata // Theoret. Comp. Sci. - 1998. - V.194. - P. 183-205.

15. Чеботарев А.Н. Метод раздельного резольвирования для проверки выполнимости формул языка L // Кибернетика и системный анализ. - 1998. - N6. - C. 13-20.

16. Чеботарев А.Н. Общий метод проверки согласованности взаимодействующих автоматов с конечной памятью // Кибернетика и системный анализ. -1999. - N6. - C. 25-37.

17. M.Perkowski, A.Chebotarev, A.Mishchenko. Evolvable Hardware or Learning Hardware? Induction of State Machines from Temporal Logic Constraints // Proc. of the First NASA/DOD Workshop on Evolvable Hardware (NASA/DOD-EH 99), Pasadena, USA, 1999. - P. 129-138.

18. Чеботарев А.Н. Об одном способе спецификации реактивных алгоритмов в логическом языке первого порядка // Проблемы программирования. - 2000. - N1,2. - C. 273-279.

19. Chebotarev A.N. Provably-correct development of reactive algorithms // Proc. Int. Workshop: Rewriting Techniques and Efficient Theorem Proving (RTETP-2000), Kyiv. - 2000. - P. 117-133.

20. Капитонова Ю.В., Чеботарев А.Н. Индуктивный синтез автомата по спецификации в логическом языке L // Кибернетика и системный анализ. - 2000. - N6. - C. 3-13.

21. Чеботарев А.Н. Построение автомата (распознавателя) по формуле монадической теории первого порядка для натуральных чисел // Кибернетика и системный анализ. - 2001. - N4. - C. 91-106.

22. Чеботарев А.Н. Теоретико-автоматный подход к верификации реактивных систем // Кибернетика и системный анализ. - 2001. - N6. - C. 37-49.

23. Чеботарев А.Н., Алистратов О.В. Построение логической спецификации реактивного алгоритма // Проблемы программирования. - 2002. - N1,2. - C. 154-160.

24. Чеботарев А.Н. Использование дедуктивных построений для проектирования алгоритмов // Методы алгоритмизации и реализации процессов решения интеллектуальных задач. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1986. - C. 4-11.

25. Чеботарев А.Н. Об одном методе абстрактного синтеза автоматов с конечной памятью // Методы и средства проектирования дискретных систем. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1988. - C. 4-12.

26. Чеботарев А.Н. Функциональное проектирование автоматов // Интеллектуализация программного обеспечения информационно-вычислительных систем. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1990 - C. 12-17.

27. Мороховец М.К., Чеботарев А.Н. Программная поддержка синтеза автомата по спецификации // Интеллектуальные инструментальные программные средства. Киев: Ин-т кибернетики им. В.М.Глушкова НАН Украины, 1993. - C. 10-18.

28. Чеботарев А.Н. Использование логики первого порядка для спецификации и синтеза автоматов // Тр. II Всесоюз. конф. по прикладной логике. Новосибирск: ИМ СО АН СССР, 1988. - C. 242-243.

Чеботарьов А.М. Доказове проектування алгоритмів функціонування реактивних систем. - Рукопис.

Дисертація на здобуття наукового ступеня доктора технічних наук за спеціальністю 05.13.13 - обчислювальні машини, системи та мережі, Інститут кібернетики ім. В.М.Глушкова НАН України, Київ, 2002.

Розроблено загальну теорію та методологію доказового проектування реактивних алгоритмів на початкових етапах їхньої розробки. Запропонований підхід до доказового проектування базується на методах синтезу відкритих систем і гарантує точну відповідність одержаного алгоритму його специфікації в логічній мові першого порядку.

Ключові слова: реактивні системи, доказове проектування, логічні мови першого порядку, взаємодіючі системи, синтез автоматів, верифікація.

Чеботарев А.Н. Доказательное проектирование алгоритмов функционирования реактивных систем. - Рукопись.

Диссертация на соискание ученой степени доктора технических наук по специальности 05.13.13 - вычислительные машины, системы и сети, Институт кибернетики им. В.М.Глушкова НАН Украины, Киев, 2002.

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

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

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

Впервые сформулирована проблема детерминизации логических спецификаций и получено математически обоснованное ее решение.

Сформулирована в новой постановке проблема обеспечения корректного взаимодействия между проектируемой системой и внешней средой. Получено эффективное решение этой проблемы на основе теоретико-автоматных и логических методов.

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

Ключевые слова: реактивные системы, доказательное проектирование, логические языки первого порядка, взаимодействующие системы, синтез автоматов, верификация.

Chebotarev A.N. Provably-correct development of algorithms of reactive systems operation. - Manuscript.

Thesis in fulfillment of the requirements for the degree of Doctor of engineering sciences on speciality 05.13.13 - computers, systems and nets. Glushkov Institute of Cybernetics of National Academy of Sciences of Ukraine, Kyiv, 2002.

The general theory and methodology of provably-correct design of reactive algorithms at the initial stages of their design is developed. The proposed approach to provably-correct design is based on methods of open systems synthesis and guarantees the strict correspondence of the algorithm obtained to its specification in a first-order logic language.

Key words: reactive systems, provably-correct design, first-order logic languages, interacting systems, automata synthesis, verification.

Размещено на Allbest.ru