Содержание к диссертации
Введение
1. Определения, обозначения, обзор литературы 15
1.1. Устройства управления техническими объектами 15
1.1.1. Синтез цифровых устройств управления 15
1.1.2. Контроллеры 17
1.1.3. Корректировка алгоритма управления 22
1.2. Основные определения и обозначения 24
1.2.1. Конечные автоматы 24
1.2.2. Отношения между автоматами 30
1.2.3. Полностью определенные формы автомата 34
1.2.4. Синхронная композиция конечных автоматов 39
1.2.5. Пример конечно-автоматного компенсатора 44
1.2.6. Синтез компенсаторов и автоматные уравнения 45
1.3. Известные методы решения автоматных уравнений для топологии контроллера 46
1.3.1. Алгоритм нахождения наибольшего решения автоматного уравнения 47
1.3.2. Алгоритм решения автоматного уравнения на основе отношения моделирования 50
1.3.3. Сложность решения автоматного уравнения для топологии контроллера 52
1.3.4. Синтез оптимальных компенсаторов 53
1.3.5. Синтез тестов для конечно-автоматных компенсаторов 54
1.4. Выводы по ГЛАВЕ 57
2. Синтез оптимального компенсатора для абстрактных автоматов 58
2.1. Эквивалентность разрешимости уравнений для топологии контроллера и последовательной топологии 60
2.2. Синтез наибольшего решения для полностью определенных детерминированных автоматов 63
2.3. Синтез наибольшего согласованного конечно-автоматного компенсатора 67
2.4. Минимальные детерминированные редукции недетерминированных автоматов 72
2.4.1. Редукции и подавтоматы 72
2.4.2. r-несовместимые состояния 73
2.4.3. Сохраняемое покрытие автомата 77
2.4.4. Достаточное условие эквивалентности минимальной редукции некоторому подавтомату исходного автомата 80
2.4.5. Алгоритм построения редукции недетерминированного автомата с наименьшим числом состояний, эквивалентной подавтомату 81
2.5. Выводы по ГЛАВЕ 82
3. Синтез оптимального компенсатора для последовательной композиции автоматов 84
3.1. Синтез компенсатора для последовательной композиции абстрактных автоматов 84
3.2. Синтез компенсаторов для микропрограммных автоматов 90
3.2.1. Микропрограммные автоматы и композиции микропрограммных автоматов 90
3.2.2. Наибольший микропрограммный компенсатор 92
3.2.3. Оптимальный микропрограммный компенсатор 93
3.2.4. Эксперименты по синтезу оптимальных компенсаторов для микропрограммных автоматов 94
3.3. Синтез компенсатора для структурных автоматов 96
3.3.1. Решение уравнения для последовательной композиции комбинационных схем 96
3.3.2. Структурные автоматы и последовательная композиция структурных автоматов 99
3.3.3. Решение уравнения для последовательной композиции автоматов с памятью 101
3.4. Выводы по ГЛАВЕ 106
4. Синтез тестов для конечно-автоматных компенсаторов 107
4.1. Синтез проверяющих тестов при безусловном эксперименте с проверяемым автоматом 108
4.1.1. Отличающий автомат 108
4.1.2. Описание отличающего автомата 109
4.1.3. Построение проверяющего теста 111
4.1.4. Сокращение длины проверяющего теста 111
4.2. Результаты экспериментов 114
4.3. Метод тестирования на основе условного эксперимента с проверяемым автоматом 116
4.4. Сокращение функции неисправности 120
4.5. Выводы по главе 122
Заключение 122
Список литературы 126
- Отношения между автоматами
- Синтез наибольшего решения для полностью определенных детерминированных автоматов
- Синтез компенсатора для последовательной композиции абстрактных автоматов
- Метод тестирования на основе условного эксперимента с проверяемым автоматом
Введение к работе
Общая характеристика работы
Актуальность проблемы. Из всех этапов проектирования дискретных систем
алгоритмическое и логическое проектирование управляющих систем наиболее
трудно поддаются автоматизации вследствие их сложности. В последнее 50-летие САПР систем логического управления на основе различных формальных спецификаций были разработаны представителями школ Гаврилова М.А., Глушкова В.М., Закревского А.Д., Агибалова Г.П., Чистова В.П., Брайтона Р., Санджиованни-Винчентелли А. и других [1-13]. Большие возможности для реализации систем управления открыли достижения микроэлектроники. Современные устройства управления технологическими процессами (контроллеры) обычно реализуются на базе микропроцессорной техники, или по принципу жесткой логики, т.е. на базе микроэлектронных ИС разной степени интеграции [14-17].
В последнее время появился ряд работ [18-25], направленных на возможность использования ранее созданных устройств управления с добавкой специального «корректирующего автомата». Такая ситуация часто возникает при модернизации устаревших устройств управления. В ряде случаев достаточно синтезировать подходящий «корректирующий автомат», компенсатор, таким образом, чтобы его совместное поведение со старым устройством управления удовлетворяло необходимым требованиям, т.е. можно говорить о синтезе управляющего автомата путем специальной декомпозиции, одна из компонент которой известна. Соответствующая декомпозиция может быть получена на основе решения автоматного уравнения. Однако, решения, предлагаемые в работах [18-20], не содержат описания всех возможных альтернатив, удовлетворяющих заданным требованиям, что, в частности, не позволяет строить оптимальные в различных смыслах компенсаторы, а соответственно и управляющие, автоматы. Кроме того, решения предлагаются только для абстрактных полностью определенных автоматов, в то время как для описания поведения
реальных устройств управления используются микропрограммные и структурные автоматы. Данная работа продолжает исследования в этом направлении и посвящена разработке алгоритмов синтеза и тестирования оптимальных конечно-автоматных компенсаторов.
Цель работы состоит в разработке технологии синтеза оптимальных конечно-автоматных компенсаторов совместно с набором проверяющих тестов. Методы исследования. Для достижения поставленной цели применяется аппарат дискретной математики, теории автоматов, теории множеств и математической логики, а также средства компьютерного моделирования для оценки эффективности разработанных методов.
Научная новизна. Предложены два подхода к полному описанию множества конечно-автоматных компенсаторов для специальной топологии автоматной сети, называемой топологией контроллера [21]. Во-первых, показано, что если поведение старого устройства управления, известной компоненты декомпозиции, описано детерминированным автоматом, то корректирующий автомат, компенсатор, можно выбрать таким, чтобы его поведение не зависело от выхода управляющего автомата. Иными словами, автомат-компенсатор можно синтезировать для композиции без обратной связи. Однако в этом случае компенсатор может оказаться более сложным. Поэтому для топологии контроллера предложен метод построения недетерминированного автомата, редукции которого и только они могут быть выбраны в качестве корректирующего автомата. Предложенный метод адаптирован для случая, когда поведение известной компоненты описывается частичным автоматом. В этом случае компенсатор должен быть согласован с корректируемым автоматом, т.е. его выходные последовательности должны быть допустимыми для корректируемого устройства. Технология декомпозиции управляющих автоматов адаптирована на случай микропрограммных и структурных автоматов.
Под оптимальным компенсатором в работе понимается автомат-компенсатор с минимальным числом состояний. Как известно [26-27], построение такого
6 автомата-компенсатора связано с нахождением минимальной
ш детерминированной редукции недетерминированного автомата. Предложены
достаточные условия, при которых такая редукция эквивалентна подавтомату
исходного автомата, и предложен алгоритм нахождения минимальной
редукции в этом случае.
Предложен метод синтеза проверяющего теста для
недетерминированного автомата, основанный на условном эксперименте с
детерминированной реализацией. Предложенный метод может быть
* использован для синтеза тестов для конечно-автоматных компенсаторов.
Достоверность результатов. Все научные положения и выводы,
содержащиеся в диссертации, основаны на утверждениях, доказанных с
использованием аппарата общей алгебры и теории конечных автоматов.
Практическая ценность работы. Методы, разработанные в диссертации,
могут использоваться в системах логического синтеза дискретных
управляющих систем, в том числе для их оптимизации и диагностики.
ф Реализация полученных результатов. Исследования, результаты которых
изложены в настоящей диссертации, проводились в рамках следующих
грантов и научно-исследовательских проектов.
а Грант РФФИ 99-01-00337 "Решение автоматных уравнений и неравенств".
а Программа МО РФ 2000 г. "Научные исследования высшей школы в
области производственных технологий", раздел "Интеллектуальные
системы автоматизированного проектирования и управления
ft производством", НИР "Разработка интеллектуальной системы
автоматизированного проектирования и тестирования цифровых
контроллеров". а Обменный Грант НАТО PST.CLG 979698 «Logic synthesis and analysis
through automata and FSM equation solving» совместно с университетом
Беркли США (Научная группа проф. Р. Брайтона). Программа «Университеты России» УР.04.01.018. «Алгебра автоматов и
полуавтоматов: отношения, операции, решение уравнений и неравенств».
Результаты проведенных исследований включены в курс лекций по теории автоматов, которые читаются на радиофизическом факультете ТГУ. Апробация работы. Результаты, вошедшие в работу, обсуждались на заседаниях совместного семинара кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ, кафедр программирования и защиты информации и криптографии факультета прикладной математики и кибернетики ТГУ. Кроме того, они докладывались на конференциях, в том числе международных, в Новосибирске, Воронеже, Иркутске, Саратове, Белеке (Турция) и Томске.
Публикации. По теме диссертации опубликовано 10 печатных научных работ, из них 2 статьи в журнале «Вестник ТГУ», 2 рецензируемых доклада и 6 тезисов докладов в трудах Российских и международных конференций. Структура и объем диссертации. Диссертация состоит из введения, четырех глав, заключения и списка цитированной литературы. Объем диссертации составляет ... страниц текста, набранного в редакторе MS Word 97 (Шрифт -Times New Roman Cyr, размер шрифта - 14 pt, межстрочный интервал — 1,5 строки), в том числе: титульный лист - 1с, оглавление - 2с, основной текст, включающий 34 рисунка, - 124с, библиографический список из 109 наименований - 1 Ос.
Основное содержание работы
Чтобы систематизировать изложение материала и облегчить его восприятие, в
работе принято разбиение на главы, разделы, параграфы и пункты. Первая глава диссертации содержит необходимые понятия и определения теории автоматов, постановку задачи, а также краткий обзор публикаций по теме диссертации. В первом разделе главы приводится краткий обзор публикаций по автоматизированному синтезу дискретных управляющих систем. Отмечается, в частности, что САПР систем логического управления на основе конечно-автоматных спецификаций были разработаны представителями школ Гаврилова М.А., Глушкова В.М., Закревского А.Д., Брайтона Р., Санжиованни-Винчентелли А. и других [1-13]. Кратко описываются
современные устройства управления технологическими процессами (контроллеры), которые обычно реализуются на базе микропроцессорной техники. Подчеркивается, что в данной работе исследуется проблема синтеза корректирующего автомата для устройств управления, т.е. исследуется проблема декомпозиции конечного автомата в сеть из двух компонент, одна из которых известна.
Конечные автоматы представляют специальный класс функций, которые сопоставляют каждому слову во входном алфавите одно или несколько слов той же длины в выходном алфавите. В общем случае такая функция может быть определена на бесконечном множестве входных слов, однако использование конечных автоматов позволяет описать ее конечным образом. Таким образом, при помощи конечного автомата удобно представлять поведение систем, преобразующих последовательности дискретных входных сигналов в последовательности выходных сигналов. В разделе 1.2 приведены формальные определения из теории автоматов. В работе рассматриваются отношения эквивалентности и редукции, которые формально описывают требования к синтезируемому автомату. Вводится операция синхронной композиции автоматов. Операция синхронной композиции считается достаточно простой операцией, однако в [28] показано, что все другие операции, в том числе асинхронной композиции, могут быть получены посредством этой операции, если во все алфавиты ввести так называемый «молчащий» символ, который соответствует отсутствию символа в канале. Последний параграф раздела 1.2 содержит постановку задачи. Обычно входами корректирующего автомата являются внешние входы синтезируемого устройства и выходы корректируемого устройства, т.е. топология декомпозиции управляющего автомата, называемая в [21] топологией контроллера, определена. Известно, что задача синтеза корректирующего автомата, который в англоязычной литературе часто называется контроллером или компенсатором [21-25], сводится к решению автоматного уравнения для топологии контроллера. Мы в нашей работе используем понятие
компенсатора, т.к. в русскоязычной литературе под контроллером обычно понимается устройство управления, реализованное на базе микропроцессорной техники [14-17]. Синтез оптимального компенсатора соответственно сводится к нахождению оптимального решения автоматного уравнения для так называемой топологии контроллера, когда входами синтезируемого контроллера являются внешние входы сети и выходы корректируемого автомата [21]. Обзор публикаций, относящихся к построению компенсатора на основе решения соответствующего уравнения, приведен в разделе 1.3. В работах [21-23] задача, поставленная в [24] усложняется тем, что синтезируемый управляющий автомат может быть недетерминированным. В работе [25] задача обобщается введением "возмущений", т.е. решается для случая, когда некоторые входы управляемого автомата недоступны для компенсатора. Алгоритм поиска одного решения автоматного уравнения, если таковое существует, предлагается в работах [18-20]. В работах [12,29] показано, что разрешимое автоматное уравнение для топологии контролера имеет наибольшее решение. Формально, любой автомат-компенсатор есть редукция наибольшего решения. Таким образом, наибольшее решение можно считать «резервуаром», который содержит все возможные конечно-автоматные компенсаторы. Однако [12], не каждый автомат из этого резервуара может быть использован при декомпозиции управляющего автомата, т.е. вопрос о точном описании множества всех конечно-автоматных компенсаторов остается открытым. Таким образом, для синтеза оптимального компенсатора приходится перебирать элементы резервуара, количество которых экспоненциально зависит от размеров наибольшего решения. Практически такой перебор во многих случаях не осуществим. Поэтому одной из основных не решенных задач является задача ограничения (если возможно) наибольшего решения таким образом, что все его полностью определенные редукции, и только они могли быть использованы в качестве компенсатора в декомпозиции управляющего автомата. Отмечается также, что, все методы решения автоматных уравнений развиты для абстрактных автоматов, в то время как для
описания реальных систем используются микропрограммные и структурные автоматы, для которых разработанные методики необходимо адаптировать. Более того, синтезированный конечно-автоматный компенсатор необходимо обеспечить набором проверяющих тестов. Проверяющий тест для автомата-компенсатора можно строить как тест для недетерминированного эталона (наибольшего решения автоматного уравнения) относительно редукции [30-37]. В разделе 1.3.5 даны определения модели неисправности и полного проверяющего теста, а также приведен краткий обзор по синтезу полных проверяющих тестов для недетерминированных автоматов как на основе безусловного [30-37], так и условного экспериментов с проверяемым автоматом [38-40].
Во второй главе предлагаются методы синтеза оптимального компенсатора для абстрактных автоматов. Как следует из приведенного в главе 1 обзора, если для полностью определенных автоматов конечно-автоматный компенсатор существует, то существует и наибольший компенсатор. Однако не всякая редукция, в том числе полностью определенная, наибольшего компенсатора является компенсатором, что во многих случаях затрудняет синтез оптимального компенсатора, а иногда делает это невозможным. Причиной является тот факт, что, несмотря на разрешимость автоматного уравнения, т.е. существование наибольшего решения, которое является недетерминированным автоматом, не существует детерминированного конечно-автоматного компенсатора. Мы предлагаем два решения этой проблемы. Во-первых, в разделе 2.1 показано, что если существует компенсатор для детерминированного автомата, то его можно выбрать таким, что поведение компенсатора не зависит от выхода корректируемого автомата. Иными словами, компенсатор можно синтезировать для последовательной композиции, которая иногда оказывается более надежной, например, в смысле отказоустойчивости [12]. Кроме того, для последовательной композиции, любая полностью определенная редукция наибольшего решения соответствующего уравнения является конечно-автоматным компенсатором,
11 т.е. оптимальный компенсатор можно выбрать, как редукцию
недетерминированного автомата, наибольшего решения уравнения, с
необходимыми свойствами, например, как редукцию с минимальным числом
состояний [26]. Однако конечно-автоматный компенсатор для
последовательной композиции может оказаться более сложным. Поэтому
предлагается ограничить наибольшее решение уравнения таким образом,
чтобы всякая его редукция была автоматом-компенсатором. Технология
такого ограничения предлагается в разделе 2.2. В разделе 2.3 технология
адаптируется для частичных автоматов. В случае, когда поведение
корректируемой системы описано частичным автоматом, в качестве
компенсатора можно выбирать только автоматы, поведение которых
согласовано с корректируемым автоматом. Иными словами, выходные
последовательности автомата-компенсатора должны быть допустимыми для
системы, поведение которой корректирует компенсатор. В разделе 2.4
обсуждаются способы построения конечно-автоматного компенсатора с
наименьшим числом состояний. Как известно [26], построение такой редукции
тесно связано с понятием сохраняемого покрытия в недетерминированном
автомате и, кроме того, такая редукция является подавтоматом автомата,
множеством состояний которого являются подмножества состояний
исходного автомата [26]. В разделе 2.4. предлагается достаточное условие,
когда минимальную редукцию можно искать среди подавтоматов исходного
автомата, и предложен метод построения такой редукции. Результаты
проведенных компьютерных экспериментов показывают, что предложенный
метод является эффективным, т.е. доставляет минимальную редукцию, а в
случае, когда минимальная редукция не эквивалентна подавтомату исходного
автомата, доставляет редукцию, близкую к минимальной.
В третьей главе рассматривается синтез оптимального конечно-автоматного
компенсатора для последовательной композиции, для абстрактных,
микропрограммных и структурных автоматов. В разделе 3.1 предлагается
оригинальная формула для синтеза наибольшего решения автоматного
уравнения в случае последовательной композиции. На основе предложенной формулы исследован ряд частных случаев на предмет существования или не существования конечно-автоматного компенсатора. В практических ситуациях для описания поведения цифровых устройств управления используют так называемые микропрограммные автоматы, которые отличаются от абстрактных автоматов тем, что имеют структурные входной и выходной алфавиты, т.е. входной и выходной алфавиты микропрограммного автомата суть множества булевых векторов. Кроме того, все переходы обычно описываются на множествах интервалов входных и выходных переменных. В англоязычной литературе микропрограммному описанию автомата можно соотнести описание в так называемом KISS-формате [41]. Синтезу компенсаторов для микропрограммных автоматов посвящен раздел 3.2. Вводится понятие недетерминированного микропрограммного автомата. Предлагаются алгоритмы нахождения наибольшего решения уравнения для микропрограммных автоматов и нахождения оптимального автомата-компенсатора, как оптимального подавтомата наибольшего решения. Компьютерные эксперименты, проведенные на контрольных примерах из сети ИНТЕРНЕТ (benchmarks) [42], показали, что предложенные алгоритмы достаточно эффективны.
В структурном автомате входные и выходные символы, а также состояния автомата, являются двоичными векторами. В этом случае функции переходов и выходов можно представить как соответствующие системы булевых функций, что во многих случаях обеспечивает более компактное представление автомата. Иногда такое представление автомата называют каноническим [43-44]. В разделе 3.3 рассматривается задача синтеза конечно-автоматного компенсатора для случая, когда корректируемый автомат и синтезируемый управляющий автомат являются структурными автоматами, т.е. их поведение описывается системами булевых функций. В первой части раздела 3.3 автомат-компенсатор синтезируется для автомата без памяти, т.е. комбинационной схемы. Во второй - предложен метод синтеза конечно-
автоматного компенсатора (если существует) для случая произвольных структурных автоматов.
Четвертая глава посвящена синтезу условных проверяющих тестов для
недетерминированного автомата относительно редукции. Как было отмечено
выше, синтезированный конечно-автоматный компенсатор желательно
обеспечить набором проверяющих тестов. Согласно результатам раздела 1.3,
компенсатор есть редукция наибольшего решения автоматного уравнения,
которое в общем случае является недетерминированным автоматом. Таким
образом, в процессе тестирования необходимо определить, является ли
синтезированный автомат-компенсатор редукцией заданного
недетерминированного автомата. Потому тесты для автомата-компенсатора нужно строить как тесты для недетерминированного эталона (наибольшего решения уравнения) относительно отношения редукции [30-37]. Методы синтеза таких проверяющих тестов в последнее время активно развиваются [35-37]. Однако, как следует из результатов проведенных экспериментов, эти методы доставляют очень длинные и часто избыточные тесты. Поэтому в данной работе мы предлагаем метод синтеза теста, основанный на условном эксперименте [38-40] с проверяемым автоматом. При условном эксперименте каждая следующая тестовая последовательность выбирается на основе реакций проверяемого автомата на предыдущие последовательности. Как известно [40], условные тесты обычно короче безусловных тестов.
В разделе 4.1 мы приводим основные детали метода из [36] построения безусловного полного проверяющего теста для недетерминированного эталона относительно редукции, часть из которых будет использована для синтеза теста при условном эксперименте. В разделе 4.2 приводятся результаты проведенных нами компьютерных экспериментов по оценке длины безусловного теста. Проведенные эксперименты показали, что для автоматов, число состояний и входных символов которых больше 10, тесты являются слишком длинными. В параграфах 4.3 и 4.4 предлагается оригинальный метод построения условного проверяющего теста, который основан на
детерминизации эталонного недетерминированного автомата и сокращении области неисправности на основе реакций проверяемого автомата на предыдущие тестовые последовательности.
В заключении подводится итог результатам, полученным в диссертационной работе, и формулируются основные положения, выносимые на защиту.
Отношения между автоматами
В данной работе мы будем интересоваться синтезом компенсаторов для систем, поведение которых описывается конечными автоматами. Выходная реакция синтезируемой системы на любую допустимую входную последовательность должна содержаться в множестве эталонных реакций, « которое мы будем представлять посредством так называемого эталонного автомата или спецификации. Формально такое отношение между системами можно описать посредством отношений эквивалентности и редукции. При отношении редукции [91] требуется, чтобы синтезируемая система делала "не больше", чем спецификация, в то время как отношение эквивалентности [85] требует, чтобы синтезируемая система выполняла в точности то же самое, что и спецификация. Автомат B=(T,I,O,G,t0) называется подавтоматом автомата A-{S,I,O,H,s0), если TczS и GczH. Автоматы А и В равны, если А является подавтоматом В, а.В- подавтоматом А. Очевидно, что два автомата равны тогда и только тогда, когда совпадают их входные и выходные алфавиты, множества состояний, начальные состояния и отношения поведения. Детерминированный автомат, поведение которого содержится в поведении данного недетерминированного автомата, называется редукцией последнего. Формально отношение редукции между автоматами определяется следующим образом. Состояние t автомата B=(T,I,O,G,t0) называется редукцией состояния s автомата A=(S,I,O,H,s0) (обозначение: t s), если язык автомата В в состоянии / содержится в языке автомата А в состоянии s. Для автоматных отображений отношение редукции определяется следующим образом. Состояние / автомата В является редукцией состояния s автомата А, если область определения 3B{t) автомата В в состоянии / есть подмножество в области определения 3A{s) автомата А в состоянии s, и для любой входной последовательности ae3B(f) выходная последовательность уеО автомата В содержится в множестве выходных последовательностей автомата А на последовательность а; в противном случае состояние / не является редукцией состояния s (обозначение: ts). Если состояние / есть редукция состояния s, и состояние s есть редукция состояния /, то состояния t и s называются эквивалентными (обозначение: t=s). Языки автоматов в эквивалентных состояниях совпадают. Автомат А называется приведенным [90], если его состояния попарно не эквивалентны. Автомат В называется редукцией [85,90] автомата А (обозначение: В А), если начальное состояние В есть редукция начального состояния А, в противном случае В не есть редукция А (обозначение: ВА). Если автомат А является наблюдаемым, то для проверки, является ли детерминированный автомат В редукцией автомата А, можно воспользоваться пересечением [92] этих автоматов. Пусть A=(SJ,OJf,so) и B=(TJ,0,G,qo) - автоматы. Построим пересечение Аг\В автоматов А и В. Пересечением АпВ автоматов А и В называется наибольший связный подавтомат автомата (SxTJ,0,F,s0to), в котором отношение F определено следующим образом: (st,i,o,s t )eF = (s,i,o,s )eH & (t,i,o,t )eG. По определению, множество входо-выходных последовательностей автомата Аг\В есть пересечение соответствующих множеств автоматов А и В. Если автоматы А и В наблюдаемые, то их пересечение также является наблюдаемым автоматом. Однако пересечение полностью определенных автоматов может быть частичным автоматом, т.к. поведение автоматов может совпадать не для всех входных последовательностей. Пусть детерминированный автомат В не является редукцией наблюдаемого автомата А. Тогда существуют состояние s автомата А, состояние / автомата В и входной символ / такие, что на входной символ / автомат В в состоянии t выдает выходной символ, который невозможен для автомата А в состоянии s. Поэтому переход пересечения Аг\В на входной символ / в состоянии st не определен. Таким образом, справедливо следующее утверждение. Утверждение 1.1 [92]. Детерминированный автомат В является редукцией наблюдаемого автомата А, если и только если для каждого состояния st пересечения АпВ и любого входного символа /, на котором определено поведение автомата В в состоянии /, поведение автомата АпВ определено в состоянии st на входном символе /.
Рассмотрим автоматы А я В, изображенные на рис. \.5а и \.5Ь соответственно. Определим, является ли автомат В редукцией автомата А. Автомат АпВ их пересечения изображен на рис. 1.5с. а) Ъ) Как видно, в состояниях SQ и to на входной символ іг множество {0} реакций автомата А не содержит множество {1} реакций автомата В, и, как следствие, поведение пересечения АслВ автоматов не определено в начальном состоянии для входного символа І2, таким образом, автомат В не является редукцией автомата Л.
Синтез наибольшего решения для полностью определенных детерминированных автоматов
Пусть A=(S, V,O,H,s0) и C=(Q,I,0,G,qo) -автоматы, представляющие контекст и спецификацию, и М - наибольшее полностью определенное решение уравнения Х»А=С для топологии контроллера, т.е. М - наибольший компенсатор, построенный по алгоритму 1.1. В качестве примера рассмотрим автоматы на рис. 1.14. Наибольший компенсатор приведен на рис. 1.15а. Непосредственной проверкой можно убедиться, что редукция наибольшего компенсатора на рис. 1.156 в композиции с контекстом есть частичный автомат. Таким образом, не все детерминированные редукции наибольшего компенсатора могут быть использованы в качестве компенсатора. В данном параграфе мы предлагаем метод сокращения наибольшего компенсатора таким образом, что любую полностью определенную редукцию сокращенного наибольшего компенсатора можно использовать в качестве компенсатора.
Исследуя выше приведенный пример, можно заметить, что композиция компенсатора и корректируемого автомата получилась частичной за счет того, что в состоянии С\ для входного символа i\0\ мы выбрали переход в «безразличное» состояние Trap. Поскольку спецификация является детерминированным автоматом, в каждом состоянии наибольшего компенсатора для каждого входного символа / существует единственный выходной символ о такой, что переход из данного состояния под действием пары io определен не в «безразличное» состояние. Для того чтобы получить редукцию наибольшего компенсатора, которая в композиции с автоматом А будет полостью определенным автоматом, необходимо и достаточно на этом переходе выбрать переход в любое, кроме «безразличного», состояние. Таким образом, чтобы не иметь лишних редукций, которые не являются решениями уравнения для топологии контроллера, мы не добавляем в множество переходов наибольшего компенсатора М переход в состояние Trap для входного символа и состояния, если для них уже существует определенный переход. Заметим, что, вообще говоря, сказанное выше справедливо не только для детерминированных решений уравнения, но и для любой полностью определенной редукции. Поэтому далее ограничение, построенное по алгоритму 2.1, называется корректным наибольшим компенсатором.
Таким образом, для построения корректного наибольшего компенсатора, не содержащего «лишние» редукции, мы предлагаем следующий алгоритм. Алгоритм 2.1. Построение корректного наибольшего компенсатора для автомата А при спецификации С, все полностью определенные редукции которого, и только они являются решениями автоматного уравнения Х»А=С Вход: автомат A=(S, V,0,H,so) и спецификация C=(Q,I,O,F,q0). Выход: корректный наибольший компенсатор (если компенсатор существует). Шаг 1. Построим автомат (P j{Trap}JxO,V,Z,p0), в котором P-QxS, /?о=( оЛ)5 ZQ(F\j{Trap})x(IxO)xVx(Pu{Trap}) и для любых /є/, оеО,реР справедливо: 1) {(q,s),io,v,{q ,s ))eZ, если и только если (q,i,o,q )eF & (q,v,o,q )eH; 2) Четверка ((q,s),io,v,Trap)eZ, если и только если не существует q Q такого, что (q,i,o,q )eF; 3) В состоянии Trap добавляем петлю, помеченную всеми входо-выходными парами. Шаг 2. Последовательно удаляем из автомата, получившегося на шаге 1, состояния, в которых не определен хотя бы один переход и все переходы в такие состояния. Если удаляется начальное состояние, то компенсатора для автомата А при спецификации С не существует. В противном случае получаем недетерминированный автомат, множество полностью определенных детерминированных редукций которого совпадает с множеством всех компенсаторов. Теорема 2.2. Пусть А и С суть полностью определенные детерминированные автоматы с равными выходными алфавитами и Л/ -решение, построенное по алгоритму 2.1. Полностью определенный детерминированный автомат В является компенсатором для автомата А при спецификации С, если и только если В есть редукция автомата М. Доказательство. Необходимость. Пусть полностью определенный детерминированный автомат В является компенсатором для автомата А при спецификации С. Обозначим через ЛА, Лв, Лс функции выходов автоматов А, В, С соответственно. Рассмотрим произвольную входную последовательность аєі . Пусть автомат С на последовательность а реагирует последовательностью /?є О , Лс(сс)=/3, и автомат В на последовательность а/3 щ реагирует последовательностью уе V , т.е. Хв{р.р)-у. Согласно алгоритму 2.1, пара aft/у есть входо-выходная последовательность корректного наибольшего компенсатора М. Если мы рассмотрим продолжения последовательностей ai и fh такие, что и Xc(ai) fh, то, согласно алгоритму 2.1, любая пара (ai,j3o)/yv, veV, есть входо-выходная последовательность корректного наибольшего компенсатора М. Таким образом, автомат В есть редукция корректного наибольшего компенсатора М. Достаточность. Пусть полностью определенный детерминированный автомат В есть редукция корректного наибольшего компенсатора М, построенного по алгоритму 2.1. Пусть ael , и Ac(a)=j3 и ZB(afi)=y. Тогда А{У) Р и, следовательно, Яв.А(ос)=Лс{а), т.е. автомат В является компенсатором для автомата А при спецификации С. а Рассмотрим пример. Диаграммы переходов автоматов А и С приведены на рис. 1.14. Корректный наибольший компенсатор, построенный по алгоритму 2.1, приведен на рис. 2.5. Любая полностью определенная детерминированная редукция корректного наибольшего компенсатора является компенсатором для автомата А при спецификации С. Для сравнения наибольший компенсатор, построенный по алгоритму 1.1, приведен на рис. 1.15а.
Синтез компенсатора для последовательной композиции абстрактных автоматов
Следствие 1. Полностью определенный детерминированный автомат D есть последовательный компенсатор для автомата А при спецификации С, если и только если автомат D есть редукция автомата С»А ].
Доказательство утверждения следует из определения наибольшего компенсатора и утверждения 1.5 о том, что последовательная композиция полностью определенных детерминированных автоматов есть полностью определенный детерминированный автомат. Согласно утверждению 1.2, множество полностью определенных редукций наблюдаемого автомата, совпадает с множеством таких редукций для его наибольшего полностью определенного подавтомата. Таким образом, верно следующее утверждение. Следствие 2. Последовательный компенсатор для автомата А при спецификации С существует, если и только если автомат С А Х обладает полностью определенным подавтоматом. ь Следствие 3. Если для любого детерминированного подавтомата D автомата А х автомат C D не является полностью определенным, то не существует компенсатора для автомата А при спецификации С. Доказательство. По утверждению 1.2, множество полностью определенных редукций наблюдаемого автомата, совпадает с множеством таких редукций для его наибольшего полностью определенного подавтомата. Пусть автомат А { не обладает полностью определенным подавтоматом. Это означает, что в автомате А х существует, по крайней мере, один неопределенный переход, достижимый из начального состояния. Тогда в автомате С А Х также существует, по крайней мере, один неопределенный переход, достижимый из начального состояния. Следовательно, автомат С»А Х не обладает полностью определенным подавтоматом и по теореме 3.2. компенсатора для автомата А при спецификации С не существует. Пусть теперь автомат А 1 обладает полностью определенным подавтоматом. По утверждению 1.5, композиция полностью определенных автоматов С и А х является полностью определенной. Следовательно, автомат С А Х обладает полностью определенным подавтоматом и по теореме 3.2. компенсатор для автомата А при спецификации С существует. Рассмотрим некоторые экстремальные случаи, в которых компенсатор всегда существует и случаи, в которых не существует компенсатора для автомата А при спецификации С. Пусть спецификация C=(Q,I,0,Sc,Ac,qo) и автомат 4=(5, ,(9, , 0) - детерминированные полностью определенные автоматы. В силу следствия 2 из теоремы 3.2, компенсатор для автомата А при спецификации С существует, если автомат С»А Х обладает полностью определенным подавтоматом. Последнее, в частности выполняется, если автомат А 1 является полностью определенным. Однако условие полной определенности автомата А х можно ослабить. Автомат С А Х обладает полностью определенным подавтоматом, если в любом состоянии q спецификации С множество выходных символов есть подмножество множества выходных символов автомата А в любом состоянии. Следовательно, справедливо следующее утверждение. Утверждение 3.3. Если в любом состоянии спецификации С множество выходных символов есть подмножество множества выходных символов автомата А в любом состоянии, то компенсатор для автомата А при спецификации С существует. Доказательство. Действительно, в этом случае для любого состояния q ш и любого входного символа / автомата С существует переход в некоторое состояние с выходным символом о, а в автомате А найдутся состояние 5 и входной символ v, для которых существует переход в некоторое состояние с тем же выходным символом о. Следовательно, автомат О/Г1 является полностью определенным и по теореме 3.2. компенсатор существует. Утверждение 3.4. Если в связном автомате А существует состояние s, в котором множество выходных символов является собственным подмножеством выходных символов в любом состоянии спецификации С, то компенсатора для автомата А при спецификации С не существует. Доказательство. Действительно, в этом случае для некоторого состояния s автомата А 1, в автомате С»Л-1 существует состояние qs, достижимое из начального, такое, что для некоторого входного символа в состоянии q ш поведение автомата А 1 в состоянии s не определено. Следовательно, композиция автомата С с автоматом А 1 не содержит полностью определенных подавтоматов. Согласно следствию 2 из теоремы 3.2, компенсатора для автомата А при спецификации С в этом случае не существует. Утверждение 3.5. Если в каждом состоянии автомата А реализуется весь ш выходной алфавит и автомат А является автоматом без потери информации [43], то наибольший компенсатор для автомата А при спецификации С существует и является детерминированным автоматом. Доказательство. Существование компенсатора следует из утверждения 3.3. Поскольку автомат А является автоматом без потери информации, то автомат А 1 является детерминированным. Кроме того, автомат А является полностью определенным, т.к. в каждом состоянии автомата А реализуется весь выходной алфавит. Поэтому если автомат С есть детерминированный и полностью определенный автомат, то автомат С А Х является полностью с определенным и детерминированным. В практических ситуациях для описания поведения цифровых устройств управления используют так называемые микропрограммные автоматы, которые отличаются от абстрактных автоматов тем, что имеют структурные входной и выходной алфавиты, т.е. входной и выходной алфавиты микропрограммного автомата суть множества булевых векторов. Кроме того, все переходы обычно описываются на множествах интервалов входных и выходных переменных. В англоязычной литературе к микропрограммному описанию автомата очень близко описание в так называемом KISS-формате [41].
Метод тестирования на основе условного эксперимента с проверяемым автоматом
Дополнительно сократить длину проверяющего теста можно, исключив из автомата FF те подавтоматы, которые не эквивалентны проверяемому автомату, до построения следующей части проверяющего теста.
Рассмотрим пример. Пусть недетерминированный наблюдаемый автомат М (рис. 4.2) в качестве редукций содержит все конечно-автоматные компенсаторы, а автомат FF (рис. 4.1) описывает наиболее вероятные неисправности в компенсаторе. Оптимальный компенсатор, оптимальная редукция автомата М, представлен на рис. 4.4. Построим для него полный проверяющий тест Е методом Василевского [95] в предположении, что проверяемый автомат имеет не больше состояний. Множество Е получается следующее Е={ааа, aba, ba). Рассмотрим процесс генерации условного теста.
На первом шаге множество V входо-выходных последовательностей формируется следующим образом. Входная часть множества V суть последовательности из множества Е, которые подаются на проверяемый автомат, синтезированный компенсатор. Выходная часть множества V содержит реакции проверяемого автомата на данные входные последовательности. После проведения этой части эксперимента, из функции неисправности можно удалить «лишние» подавтоматы, т.е. подавтоматы, множество входо-выходных последовательностей которых не содержит множество V. Ни один из этих подавтоматов не может быть проверяемым автоматом. Сокращение области неисправности может быть проделано следующим образом [99].
Рассмотрим усеченное дерево преемников [43] автомата FF. Дерево строится по заданному множеству V входо-выходных последовательностей и содержит только детерминированные пути функции неисправности, т.е. . пути, по которым нет переходов из одного и того же состояния в различные состояния с различными выходными символами. Если входная часть множества V состоит из двух и более входо-выходных последовательностей, то по окончании предыдущей последовательности считаем, что автомат находится в начальном состоянии, что соответствует подаче сигнала «сброс», в котором и прикладывается следующая последовательность. Каждый детерминированный путь в таком дереве будет соответствовать проверяемому автомату. Пары «состояние, входной символ», которые присутствуют на данном пути, соответствуют детерминированным переходам в искомом автомате. Пары, которых на данном пути нет, наследуют соответствующее множество переходов из исходного недетерминированного автомата. Объединяя полученные автоматы в один автомат, получим подавтомат FF исходного мутационного автомата. При таком построении из автомата FF исключаются подавтоматы, которые не обладают заданным множеством # входо-выходных последовательностей V. Для нашего примера сокращенный мутационный автомат представлен на (рис. 4.7).Как показывает пример, мутационный автомат также становится более детерминированным, а значит, появляется возможность сократить проверяющий тест, построенный по отличающему автомату. Построим отличающий автомат FFXM для нашего примера и полный проверяющий тест для автомата FF\M методом, описанным в разделе 4.1.2. Полученный тест Е={ аа, ab, ba, bb}. Тест получается таким же, как и в случае 122 исходного автомата FF. В нашем примере сокращение функции неисправности не приводит к сокращению длины теста. Однако в некоторых случаях сокращение автомата FF приводит к сокращению длины проверяющего теста. 4.5. Выводы по главе В данной главе предлагается подход к синтезу проверяющих тестов для недетерминированных автоматов относительно редукции, которые могут быть использованы при тестировании компенсаторов, синтезированных не формальными методами. Проведенные компьютерные эксперименты (таблица 2) показали, что безусловные тесты для недетерминированных автоматов, построенные известными методами, являются слишком длинными. Причем длина теста существенно зависит от степени детерминизма, т.е. числа детерминированных переходов, как в эталонном недетерминированном автомате, так и в мутационном автомате, который представляет область неисправности. Поэтому в данной работе прелагается строить проверяющие тесты на основе условного эксперимента с проверяемым автоматом. В данной главе мы предлагаем метод построения условного проверяющего теста относительно редукции, в котором эталонный и мутационный автоматы на каждом шаге принятия решений детерминизируются на основе реакций проверяемого автомата на предыдущие входные последовательности, и как следствие, получаем более короткий проверяющий тест. Заключение Диссертационная работа посвящена разработке методов синтеза конечно-автоматных компенсаторов. Компенсатор и корректируемая система, работая совместно, должны иметь требуемое поведение, которое задается спецификацией. Поведение всех систем описывается конечными автоматами, поэтому в этом случае говорят о компенсаторе для конечного автомата (при заданной спецификации). Топология сети, в которую объединяются компенсатор и корректируемая система, известна под названием топологии контроллера. Во введении и первой главе обсуждаются известные подходы к синтезу компенсаторов для конечных автоматов, и отмечается, что задача синтеза компенсатора может быть сведена к решению автоматного уравнения для топологии контроллера. Если уравнение разрешимо, т.е. компенсатор при заданной спецификации существует, то существует и наибольший компенсатор, т.е. недетерминированный автомат, который в качестве редукций содержит все конечно-автоматные компенсаторы. Только полностью определенные детерминированные редукции этого автомата могут быть выбраны в качестве конечно-автоматного компенсатора. Однако, отмечается, что в общем случае не всякая такая редукция является решением уравнения, т.е. может быть выбрана в качестве компенсатора. Последнее является препятствием для выбора среди решений уравнения оптимального решения, т.е. препятствием для синтеза оптимального конечно-автоматного компенсатора. Кроме того, методы синтеза компенсаторов развиты только для абстрактных автоматов, в то время как для описания реальных систем используются микропрограммные и структурные автоматы. Следует также отметить, что проверяющие тесты для синтезированного компенсатора приходится генерировать как тесты для недетерминированного автомата относительно редукции. Методы синтеза тестов для недетерминированных автоматов в последнее время активно развиваются, однако известные методы доставляют слишком длинные тесты.
