Анотація до роботи:

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

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

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

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

Головною перешкодою на шляху побудови теорії і методології автоматизованого проектування алгоритмів функціонування реактивних систем є надто велика обчислювальна складність розв’язання багатьох задач проектування. Ці задачі, зазвичай, належать до класів 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.