Розв"язання проблеми забезпечення безпомилковості процесу проектування реактивних алгоритмів промислового рівня складності, що передбачає розробку математичного апарату доказового проектування алгоритмів. Розробка методів синтезу автомата-розпізнавача.
При низкой оригинальности работы "Доказове проектування алгоритмів функціонування реактивних систем", Вы можете повысить уникальность этой работы до 80-100%
Досягнути цього можна застосуванням строгих методів коректного проектування алгоритмів функціонування реактивних систем (реактивних алгоритмів), причому велике значення має забезпечення коректності алгоритму на початкових етапах його розробки, оскільки вартість усунення помилок, допущених на цих етапах, найбільш велика. У методах коректного проектування реактивних алгоритмів, які використовуються на початкових етапах їх розробки, можна виділити два основні підходи: а) формальна верифікація неформально одержаного процедурного представлення алгоритму; Деякі методи верифікації реактивних алгоритмів, зокрема методи перевірки здійсненності специфікації на моделі (model checking), так само, як і методи другого підходу, використовують процедуру синтезу автомата за логічною специфікацією властивостей алгоритму. Їхні ідеї одержали широкий розвиток, і нині методи, які використовують темпоральні логіки або інші аналогічні числення, наприклад, числення, що базуються на операторах нерухомої точки, застосовуються на усіх етапах проектування реактивного алгоритму, починаючи із специфікації, верифікації і закінчуючи формальним синтезом алгоритму. Метою дисертаційної роботи є розвязання проблеми забезпечення безпомилковості процесу проектування реактивних алгоритмів промислового рівня складності, що передбачає розробку математичного апарату доказового проектування алгоритмів і на цій основі розробку методології проектування, яка гарантує одержання такого процедурного представлення алгоритму, яке задовольняє усі вимоги до функціонування цього алгоритму.Автомат А, серед станів якого виділено одне або декілька початкових станів, називається ініціальним, у супротивному разі автомат називається неініціальним. На всіх етапах синтезу, де автомат подається у вигляді формули мови специфікації, розглядається перший елемент цієї пари, і тільки на заключному етапі, коли буде побудовано множину станів автомата, що специфікується, використовується другий елемент пари. Автомат А називається автоматом зі скінченною памяттю, якщо існує таке натуральне k, що стани, в які кожне допустиме вхід-вихідне слово довжини k переводить усі стани автомата Отже, з кожним станом qi циклічного S-автомата асоціюється множина Si всіх S-надслів, допустимих у стані qi, і множина Pi всіх зворотних S-надслів, представлених станом qi. Якщо крім того виконуються і умови 1) і 4), то нормальна форма формули F однозначно визначає автомат, який співпадає з автоматом, що специфікується формулою F.Для цього було побудовано теорію доказового проектування алгоритмів і на її основі розроблено методологію проектування, яка гарантує одержання процедурного представлення алгоритму, що задовольняє вимоги до його функціонування, сформульовані у початковій специфікації. Запропонований підхід до побудови теорії та засобів автоматизованого проектування реактивних систем полягає в розумному обмеженні класу задач, що розвязуються, такими задачами, для яких можна отримати рішення з припустимими обчислювальними витратами. Використання для інтерпретації мов множини цілих чисел замість натуральних дозволило спростити побудову специфікації алгоритму, зробити її більш природною (формули описують вимоги до поведінки системи, виходячи з історії її функціонування) і, головне, суттєво поліпшити ефективність відповідних логічних методів розвязку задач проектування. На основі цієї теореми запропоновано підхід до вибору мови верхнього рівня, який дозволяє використовувати теорему про специфікацію для побудови алгоритмів синтезу, суттєво простіших за алгоритми синтезу, які базуються на методі табло для мов темпоральних логік. Уперше в рішенні практичної задачі синтезу використовувалися топологічні властивості мови специфікації, що дозволило сформулювати обмеження на виражальні можливості мови, які призвели до значного підвищення ефективності методів синтезу.
План
ОСНОВНИЙ ЗМІСТ РОБОТИ
Вывод
Результатом дисертаційної роботи є розвязання важливої прикладної проблеми забезпечення безпомилковості процесу проектування реактивних алгоритмів промислового рівня складності на етапі побудови процедурного представлення алгоритму. Для цього було побудовано теорію доказового проектування алгоритмів і на її основі розроблено методологію проектування, яка гарантує одержання процедурного представлення алгоритму, що задовольняє вимоги до його функціонування, сформульовані у початковій специфікації.
Головною перешкодою на шляху побудови теорії і методології автоматизованого проектування алгоритмів функціонування реактивних систем є надто велика обчислювальна складність розвязання багатьох задач проектування. Ці задачі, зазвичай, належать до класів 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.
