Электронная библиотека диссертаций и авторефератов России
dslib.net
Библиотека диссертаций
Навигация
Каталог диссертаций России
Англоязычные диссертации
Диссертации бесплатно
Предстоящие защиты
Рецензии на автореферат
Отчисления авторам
Мой кабинет
Заказы: забрать, оплатить
Мой личный счет
Мой профиль
Мой авторский профиль
Подписки на рассылки



расширенный поиск

Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Галин Александр Борисович

Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний
<
Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний
>

Данный автореферат диссертации должен поступить в библиотеки в ближайшее время
Уведомить о поступлении

Диссертация - 480 руб., доставка 10 минут, круглосуточно, без выходных и праздников

Автореферат - 240 руб., доставка 1-3 часа, с 10-19 (Московское время), кроме воскресенья

Галин Александр Борисович. Диагностирование управляющих логических устройств на основе процедуры машинного доказательства теорем в исчислении высказываний : ил РГБ ОД 61:85-5/531

Содержание к диссертации

Введение

1. Анализ современных методов диагностирование цифровых устройств и программных средств 15

1.1. Методы диагностирования цифровых устройств .. 15

1.2. Методы диагностирования программных средств. 31

1.3. Выводы 35

2. Диагностирование комбинационных устройств на основе естественного логического вывода 37

2.1. Постановка задачи диагностирования комбинационных автоматов 37

2.2. Разрешающая процедура естественного логического вывода 39

2.3. Алгоритм проверки исправности комбинационного устройства 43

2.4. Алгоритм идентификации представленной модификации комбинационного устройства, 50

2.5. Алгоритм установления равносильности булевых формул 57

2.6. Проверка правильности программ, реализующих булевы функции 59

2.6.1, Сходство и различие между задачами диагностирования аппаратуры и программных средств 60

2.6.2, Методика проверки правильности лрограмвде-ализующих булевы функции 61

2.7. Выводы 67

3. Диагностирование управляющих логических устройств на основе спещального представления их структуры .. 70

3.1. Модель управляющего логического устройства... 71

3.1.1. Модель управляющей части логического устройства 73

3.1.2. Алгоритмы построения последовательностей управляющих воздействий записи и считывания информации 75

3.2. Проверка исправности путей передачи информации и совокупностей элементов памяти управляющей части логического устройства 77

3.3. .Алгоритм проверки исправности управляющего логического устройства 85

3.4. Алгоритм идентификации представленной модификации управляющего логического устройства 92

3.5. Выводы 103

4. Разработка и исследование системы диагностирование управлявдйх логических устройств .105

4.1. Елок сопряжения диагностируемого объекта с ЭВМ 106

4.2. Организация и описание комплекса прикладных программ системы диагностирования 109

4.3. Результаты использования автоматизированной системы для диагностирования управляющего логического устройства 117

4.4. Выводы 124

Заключение 126

Литература 129

Приложение, Акты о внедрении результатов работы 141

Введение к работе

Использование в народном хозяйстве все более сложных изделий и систем, реализующих современные достижения науки, техники и технологии, и резкое повышение требований к их эффективности и надежности привели к усилению интереса к технической диагностике как совокупности методов и средств, предназначенных для организации оптимальных процедур определения технического состояния объекта. Диагностирование рассматривается как некоторый специальный процесс управления и его результаты используются для активного воздействия на процессы создания, производства и эксплуатации объекта с целью повышения надежности, а следовательно, и качества продукции. Как отмечалось на 1X7 и ХХУТ съездах КПСС, решение проблемы повышения качества составляет одну из определяющих целей нашего общественно-экономического развития.

Особое место среди объектов диагностирования занимают цифровые логические устройства. Эти устройства являются ядром вычислительных систем, систем управления и обработки информации. Ответственность и важность возлагаемых на них функций резко повысили требования к надежности цифровых устройств (ЦТ), которая в значительной степени зависит от возможности организации процедур диагностирования на этапах их проектирования, изготовления и использования. Решению задач диагностирования - изучению физических свойств объектов и их дефектов, построению математических моделей объектов и моделей дефектов, анализу моделей, созданию алгоритмического обеспечения диагностических процедур, разработке аппаратных и программных средств - посвящены работы И.М.Син-деева, П.П. Пархоменко, В.И.Казначеева, А.И, Кострыкина, О.Ф.Не-молочнова, Е.С.Согомоняна, Д.В.Сперанского, М.А. Фальковича, В.П.Чипулиса, А.Г, Биргера, Е.К.Корноушенко, Д.Армстронга, М.Бре уэра, Л. Фридмана, Е.Маккласки, ДЕ. Рота и других.

В связи с повышением степени интеграции микросхем и расширением применения микросхем четвертой, пятой и шестой степени интеграции (так называемых БИС и СБИС) возможности автоматической генерации тестов и моделирования дефектов уменьшаются [ I \ . Стремление к поиску параметров, которые бы, с одной стороны, определяли поведение схемы, и, с другой стороны, легко поддавались диагностированию, и способов их диагностирования - решению задачи улучшения управляемости и наблюдаемости - привело к возникновению нового теоретического направления, известного как проектирование удоботвотируемых схем. Б рамках этого направления разрабатываются специализированные и структурные методы создания легко диагностируемых устройств. Эффективным решением этой проблемы представляется концепция самотестирования. Эта концепция заключается в том, что кристалл или схемная плата разрабатывается таким образом, чтобы обеспечивалась возможность самотестирования без участия какого-либо внешнего оборудования или программных средств [ 2 \ . Развитию этого направления посвящены работы Е.С. Согомоняна, Д.В.Сперанского, А.П.Горяшко, Т.Уильямса, К.Паркера, Дж. Хеиеса, Д.Комоницки и других.

Важное значение для обеспечения надежности изделий цифровой техники и автоматического управления имеют процедуры установления соответствия техническому заданию (проверки спецификации) и проверки исправности объекта на этапах разработки и создания опытных образцов. Проектные неисправности, вносимые на различных стадиях реализации ТЗ - при проектировании, программировании, детальном логическом проектировании и размещении логических схем, соединении элементов, а также при модификациях аппаратного и программного обеспечения, - имеют две причины: I) неполное, неоднозначное или ошибочное задание исходных требований; 2) ошибки, совершаемые на этапах претворения требований ТЗ в окончательную реализацию, т.е. в совокупность аппаратных элементов или в массив символов, представленных в цифровой форме. Исследования в области диагностирования цифровых устройств традиционно сосредоточены на поиске дефектов при производстве и эксплуатации цифровых объектов, а вопросам проверки соответствия логического проекта и прототипа функциональной спецификации уделяется мало внимания при разработке ЦУ [ 3"} , в то время как дефекты, связанные с неточностью спецификации и вносимые в процессе реализации ТЗ, составляют 70 % от общего количества дефектов, выявляемых при диагностировании [ 4 1 .

В настоящее время для выявления проектных дефектов разрабатываются тесты (вручную или с помощью автоматизированных средств) применительно к конкретным реализациям. Входным языком разрабатываемой системы тестов обычно служит графовая модель. Для осуществления частичной проверки правильности логического проекта используется логическое моделирование. В связи с тем, что детализированные имитационные модели требуют больших затрат времени на вычисление, объект моделируется по частям на основе небольшого чиола контрольных примеров. Установление правильности функционирования W в соответствии с его функциональной спецификавд-ей осуществляется о помощью функционального диагностирования. При этом разрабатываются теоты, целиком основанные на спецификации и дающие возможность проверки любой реализации ЦУ. При соответствующем ограничении этой общности оказывается возможной разработка эффективной методики диагностирования, которая будет обладать преимуществами перед существующими эвристическими процедурами [ 3 ] .

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

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

В диссертации решается задача диагностирования на этапе проектирования одного класса цифровых устройств, называемых управляющими логическими устройствами, путем разработки методов и алгоритмов проверки исправности и идентификации предъявленной модификации объекта без моделирования и генерации тестов на основе представления его структуры в виде информационной и управляющей частей, использования специального графа в качестве модели управляющей части и применения естественного логического вывода для построения процедуры машинного доказательства теорем в исчислении высказываний. Управляющие логические устройства (УЛУ) опре деляются как устройства с параллельной обработкой информации, осуществляющие управление с помощью двоичных сигналов в соответствии с заданным алгоритмом, обладающие принудительной инициализацией.

Актуальность работы связана с необходимостью создания автоматизированных способов диагностирования и проверки спецификации УЛУ без выполнения трудоемкой и дорогостоящей процедуры предварительного построения тестов.

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

Б связи с этим поставлены следующие задачи:

- разработать алгоритмы диагностирования при контроле исправности и идентификации представленной модификации комбинационного устройства;

- разработать алгоритмы диагностирования при контроле исправности и идентификации представленной модификации управляющего логического устройства на основе структурной модели объекта, состоящей из информационной и управляющей частей;

- разработать методику проверки правильности программ, реализующих булевы функции, на основе алгоритма проверки исправности комбинационного устройства;

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

Метод исследования основан на применении исчисления высказываний, теории логического вывода, теории экспериментов с автоматами, машинного доказательства теорем в исчислении высказываний и строится на сочетании формальных и содержательных подходов. Оценка сложности разработанных алгоритмов проведена на базе анализа существующих способов оценки вычислительных алгоритмов, В диссертации использованы результаты, полученные в работах Г.Генцена, В.Хао, Ф.Хилла, Ю.М.Соркина, С.Татте, Дж.Абрахама, А.Ахо, Дж.Холкрофта, дж. Ульмана.

Научная новизна результатов диссертационной работы состоит в следующем:

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

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

- уточнены оценки сложности алгоритмов и длины проверяющих и идентифицирующих последовательностей.

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

Реализация "работы. Результаты диссертации использованы в хоздоговорных работах, выполненных на кафедре прикладной математики и вычислительной техники ШСИ J& 10/80 (ГР № 80009852, инв. Ш 02.82.3028812, 02.83.0016793) и П/83 (ГР JS 01820089750), а также в работе по госбюджетной тематике "Математическое обеспечение САПР" (ГР Л 79046781, инв. JS 02.83.0045649), Разработанные методы и алгоритмы использованы при диагностировании управляющих логических устройств, при проверке правильности програми и, в частности, программы микропроцессорного устройства управления специальным технологическим процессом, при разработке автоматизированной системы диагностирования УЛУ. Технический эффект от использования материалов работы получен за счет сокращения сроков проектирования управляющих устройств на 1С$, повышения их надежности в результате замены стендовой проверки правильного функционирования изделия изделия автоматической проверкой его исправности,, уменьшения времени проверки правильности программ, реализующих булевы санкции, на 20$, сокращения сроков отладки программных средств многопроцессорного комплекса на Д# и повышения надежности управления. Ожидаемый экономический эффект от использования материалов работы составит 38 тыс,руб. в год, К защите представляются:

1, Способы диагностирования одновыходных комбинационных автоматов и управляющих логических устройств.

2, Алгоритмы проверки исправности и идентификации представленной модификации одновыходного комбинационного устройства общего вида и управляющего логического устройства.

3, Методика проверки правильности программ, реализующих булевы функции.

4, Способ реализации автоматизированной системы диагностирования управляющих логических устройств.

Материалы диссертационной работы распределены по разделам следующим образом,

В первом разделе изложены результаты анализа современного состояния проблемы диагностирования ЦТ, Рассмотрены ставшие уже "классическими" методы, применяемые при производстве и эксплуатации ЦТ, - аппаратные, программные и программно-аппаратные, а также методы проектирования контролепригодных устройств: специализированные, применяемые при создании конкретного ЦУ или системы, и структурные, решающие проблему диагностирования в общем случае. Отмечено, что использование аппарата булевых функций для описания объекта на более высоком уровне сложности - уровне функциональной структуры, введение новых способов представления диагностической информации на основе анализа соответствия "вход-выход", полученного в ходе эксперимента над объектом, применение естественного логического вывода и машинного доказательства теорем позволяют разработать процедуры диагностирования комбинационных устройств, программ, реализующих булевы функции, и УЛУ на этапе проектирования. В этом разделе также рассматриваются основные методы диагностирования программных средств. Анализируются некоторые методы проверки правильности программ на этапе проектирования. Констатируется, что поскольку теоретических основ предмета, лока не существует, часто используются эмпирические правила при проверке программ. При этом установлено, что некоторые методы диагностирования аппаратных средств могут быть перенесены в соответствующей интерпретации на программные средства.

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

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

Четвертый раздел посвящен описанию разработанной при участии автора автоматизированной системы диагностирования управляющих логических устройств, лостроенной на основе алгоритмов проверки исправности и идентификации представленной модификации комбинационных автоматов и УЛУ. Система разработана в виде комплекса прикладных программ, написанных на языке PL/I для ЕС ЭВ/1, и блока сопряжения диагностируемого объекта о ЭВМ и предназначена для диагностирования устройств на стадиях проектирования и создания опытных образцов УЛУ, эквивалентных по количеству вентилей интегральным микросхемам 4-й степени интеграции. Применение системы дает возможность отказаться от предварительного построения тестов, уменьшить время проектирования примерно на Ш?о при гарантированном отсутствии после диагностирования дефектов, связанных: с недостаточностью и неточностью спецификаций ТЗ, с согласованием микросхем между собой, а также ошибок, допущенных при разработке и технической реализации изделия.

Апробация работы. Основные результаты диссертационной работы обсуждались на:

- научно-техническом семинаре "Актуальные вопросы эффективности и качества сложных технических систем" (Москва, октябрь 1977);

- Всесоюзном семинаре "Проектирование систем диагностики" (Ростов-на-Дону, май 1978);

- семинаре "Техническая диагностика и эффективность систем управления" Ленинградского отделения Научного Совета по надежности при отделении "Механика и процессы управления" АН СССР (Ленинград, январь 1979);

- U Всесоюзном совещании по технической диагностике (Черкассы, сентябрь 1979);

- Всесоюзном семинаре "Методические вопросы проектирования систем диагностики" (Ростов-на-Дону, май 1980);

- региональном семинаре "Автоматизация проектирования электронной аппаратуры" (Таганрог, сентябрь 1981);

- Всесоюзном семинаре "Проектирование систем диагностики" (Ростов-на-Дону, май 1982).

Публикации. По теме диссертационной работы опубликовано 7 печатных работ [7, 68, 70, 84, 101, 102, 106 ] . Результаты исследований отражены также в 4-х отчетах о НИР.

Структура и объем работы, диссертационная работа состоит из введения, четырех разделов, заключения, списка использованной литературы, приложения и содержит 146 страниц текста, в том числе 19 страниц рисунков и библиографии 108 наименовании, 6 страниц приложения.

Методы диагностирования цифровых устройств

Постоянное усложнение средств вычислительной техники и автоматики предопределяло и совершенствование методов их диагностирования. Фундаментом этого совершенствования служила теория экспериментов с автоматами, получившая развитие в работах В.М. Глушкова, Я.М.Барздиня, А.М.Богомолова, В.И.Варшавского, А.Н, Скляревича, Д.В.Сперанского, А.А.Таля, В.А.Твердохлебова, Б.А. Трахтенброта, М.А.Фальковича и других. Однако при возросшей функциональной сложности дискретных объектов некоторые существенные недостатки методов теории [б, 7 J : трудность представления объекта в виде конечного автомата и исключение при этом из рассмотрения ряда свойств процессов, происходящих в реальных объектах; громоздкость я негибкость способов записи алгоритмов функционирования, а также их неприспособленность к применению машинных методов проектирования, - затрудняют решение задач диагностирования сложных цифровых устройств (ЦУ). Эти задачи требуют к себе все большего внимания ло мере возрастания сложности изделий, повышения требований к их надежности и увеличения стоимости диагностирования на всех этапах обеспечения жизненного цикла объекта.

К настоящему времени сложились три группы методов диагностирования, применяемые при производстве и эксплуатации цифровых интегральных микросхем (ИМ), устройств и систем, - аппаратные, программные и программно-аппаратные. Аппаратные методы основаны на введении аппаратурной и информационной избыточности, поэтому существующие реализации методов являются специализированными для отдельных классов ЦУ. Программные методы применяются для диагностирования программируемых устройств. Испытательные программы или тесты реализуются в перерывах функционирования объекта и (или) во время его работы как составные части рабочей программы. В некоторых случаях в качестве испытательных могут использоваться рабочие программы или их части. В последние пятнадцать лет наибольшее развитие получили программно-аппаратные методы: автоматическая генерация тестов на основе моделирования на ЭВМ поведения объекта при наличии дефектов [ 8-17] ( сигнатурный анализ Г 18-231 и генерация псевдослучайных последовательностей Г 24-28 1 .

При разработке систем генерации тестов решаются три основные задачи [29І : построение модели и определение множества неисправностей, собственно генерация тестов относительно списка отказов, моделирование устройства при наличии отказа из установленного списка В качестве модели дефекта используется одиночная константная неисправность, покрывающая и большинство кратных дефектов W Эта модель обладает следующими достоинствами: она проста и не зависит от технологии производства компонентов; для проектирования, моделирования и диагностики может использоваться одна база данных; покрытие множества неисправностей определяется путем вычисления процента проверенных дефектов. Модель объекта представляется в виде иерархически организованной структуры модельных элементов. С помощью анализа поведения исправной модели вычисляются значения ожидаемых реакций на подаваемые тестовые наборы. Моделирование схемы с отказами и сравнение вычисленных реакций с соответствующими значениями для исправной схемы дает возможность оценить качество теста. В результате рационального выбора входных наборов и реакций, обеспечивающих наибольшее покрытие списка неисправностей, удается получить близкий к оптимальному тест.

Сокращение времени моделирования и генерации тестов все еще остается очень актуальной задачей. Для повышения производительности систем генерации тестов используются модификации D -алгоритма [9, 12, 17] , параллельное и дедуктивное моделирование Г 30 1 , моделирование на уровне макромоделей Г13, 14, 311 , моделирование переходов вместо моделирования схемы [ 8 1 , применение специальных аппаратных средств для моделирования Г 32, 33 1 , исключение процедуры моделирования Г 34 1 Модификации D - алгоритма применяются для ускорения активизации путей при моделировании дефектов из заданного списка. Параллельное моделирование может уменьшить на порядок необходимое машинное время по сравнению о моделированием одиночных дефектов за один проход. При дедуктивном моделировании значительно сокращается объем вычислений за счет моделирования на каждом входном наборе только тех дефектов, которые данный набор обнаруживает. Моделирование на уровне макромоделей увеличивает скорость моделирования и повышает адекватность модели, так как при высоком уровне интеграции схем отсутствует информация о вентильной организации ИС и естественным поэтому является описание только внешнего поведения схемы. Моделирование переходов на языке описания схем (в частности, АН PL ) вместо моделирования схемы сокращает объем вычислений примерно в десять раз Г 8 J . Применение специальных машин для аппаратного моделирования - набор процессоров и блоков памяти, соединенных высокоскоростной сетью связи - значительно увеличивает скорость генерации тестов. Исключение процедуры моделирования также увеличивает быстродействие систем генерации тестов.

Разрешающая процедура естественного логического вывода

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

Исходными элементами языка натурального исчисления выска зываний служат пропозициональные переменные 01, Ь , L , ..., в содержательном смысле принимающие значения "I" или "О"; логиче ские связки - знаки 1 , & , V , э , которые определяются как одноместная (первый знак) и двуместные логические функции; скоб ки, запятые и знак секвенции —-. Пропозициональные переменные называются элементарными формулами. Формулы исчисления высказы ваний (в дальнейшем просто формулы) определяются с помощью сле дующих правил построения [ S7 J : если CL и b - элементарные формулы, то їй , lb , (CL&b), (CLVb ), (0L= b ), (Ь=»й) яв ляются формулами. Две формулы считаются эквивалентными (CL=b ), если справедливо (CL b) &, (Ь &). Подформулами данной формулы вместе с ней самой называются те формулы, которые получаются в результате ее построения. Последовательности формул, отделенные друг от друга запятыми, называются цепочками формул и обознача ются символами А , В , С Цепочки элементарных формул обозначаются символами М , N і ... . Существенным формальным элементом естественного логического вывода служит выражение которое обозначает, что В есть логическое следствие А , и называется секвенцией. Содержательный смысл секвенции Ai, ...,Arn—- В ,..., Ьа ( ,П, 0) совершенно точно определяется формулами:. 8t. А і V Ъ\ , если m 0 и П 0: V D\ , если tn=0 и П. 0 и 1 А;, если m 0 и fl. = 0 , являющимися формульными образами этой секвенции [ 88"] . Формальное различие между секвенцией и импликацией состоит в том, что антецедент (часть выражения слева от стрелки) и консеквент (часть выражения справа от стрелки) секвенции представляют собой цепочки формул, каждая из которых может быть и пустой.

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

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

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

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

Алгоритмы построения последовательностей управляющих воздействий записи и считывания информации

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

2. Метод диагностирования УЛУ, применяемый в работе, можно классифицировать как специализированный структурный, так как он обладает чертами структурных методов (разбиение структуры на информационную и управляющую чаоти, введение аппаратурной избыточности для улучшения управляемости и наблюдаемости), но является слевдализировалным поскольку применим для определенного класса объектов. Использование параллелизма в работе 7Ш, описание его управляющей части на уровне межрегистровых передач позволило упростить диагностирование устройства, несмотря на большое число его возможных состояний.

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

4. Разработанные алгоритмы 3,3 - 3.5 дают возможность проверить управляющую часть и все УЛУ в целом, обнаружить неисправности и выполнить поиск дефектов. При этом для ускорения процесса проверки исправности устройства передача информации в совокупности элементов памяти и связанные с ними комбинационные схемы информационной части УЛУ, измерение реакций объекта по различным выходам, формирования исходных секвенций и их доказательство может выполняться параллельно. Для ускорения поиска дефектов алгоритм 3.5 может выполняться по "упрощенной" схеме за счет применения специальных путей передачи информации.

5. Таким образом, использование специализированного структурного метода диагностирования, описание устройства на функциональном уровне, анализ результатов эксперимента над объектом позволяют упростить проверку исправности и поиск дефектов УЛУ за счет исключения процедур моделирования объекта и генерации тестов. Разработанные алгоритмы дают возможность ускорить процесс разработки изделия и снизить затраты на проектирование, повысить надежность устройства и увеличить достоверность управления.

Автоматизированная система диагностирования (АСД) предназначена для проверки исправности и идентификации представленных модификаций управляющих логических устройств на этапе проектирования. Система использует метод сведения задачи диагностирования УЛ7 к задаче диагностирования комбинационной логики с помощью разбиения устройств на информационную и управляющую части, описания управляющей части на уровне межрегистровых передач и применения естественного логического вывода и машинного доказательства теорем в исчислении высказываний [Ю6І .

АСД рассчитана на диагностирование объектов, эквивалентных по количеству вентилей интегральным микросхемам 4-й степени интеграции и построенных на ИГЛ серий КІЗЗ и КІ55. Применение системы дает возможность отказаться от заблаговременного построения тестов при разработке устройства, уменьшить в результате время проектирования и повысить надежность изделия. При разработке слояных многоуровневых автоматизированных систем проектирования объектов очень высокой степени интеграции Г 107 ] АСД может применяться в составе таких систем для диагностирования устройств на уровне йункционального описания. Она монет быть также использована в составе рабочей станции, подобной Г ЮаП , для разработки систем, построенных на элементах широкого применения, включая ИМ, объединенных в сложную структуру. АСД спроектирована в виде комплекса прикладных программ, написанных на алгоритмическом языке PL/ І для ЕС ЭВМ, и блока сопряжения (БС) диагностируемого объекта с ЭВМ. БС предназначен: для передачи от ЭВМ на диагностируемое устройство входных наборов, управляющих воздействий, сигналов сопровождения и их сопряжения; для передачи с диагностируемого устройства на ЭЙД выходных реакции, откликов на сигналы сопровождения; для подачи воздействий (в том числе первого набора) и снятия решщий, контролируемых оператором. Комплекс прикладних программ предназначен для автоматической проверки исправности и идентификации представленной модификации комбинационных устройств (КУ) и ОТ с помощью управляющих программ на основе алгоритмов, разработанных в разделах 2 и 3. АСД использует исходные данные в виде булевых функций и множеств управляющих воздействий, определяющих пути передачи информации.

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

Организация и описание комплекса прикладных программ системы диагностирования

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

I. Построение последовательностей управляющих воздействий записи и считывания информации для совокупностей элементов памяти УЛУ. Программа CQNSE.T по исходной информации в виде списка дуг доследовательностной диаграммы (модели управляющей части УЛУ) и инцидентных им вершин строит последовательности сигналов, управляющих записью и считыванием информации совокупностей элементов памяти (которым поставлены в соответствие вершины графа), и вычисляет мощности множеств этих последовательностей. Программа реализует алгоритмы 3,1 и 3.2.

2. Упорядочение списка значений мощностей мнокеств управляющих последовательностей выполняется программой SORT в порядке возрастания мощности значений по правилам, оговоренным при описании алгоритма 3.5.

3. Проверка исправности рабочих и специальных путей передачи информации и совокупности элементов памяти управляющей части УЛУ. Программа RI&MEM по исходной информации в виде результатов работы программы C0NSET я таблицы соответствий " ST] -входные переменные" проверяет правильность занесения информации "шахматный код" в элементы памяти УЛУ через рабочие и специальные пути передачи информации и определяет область возникновения дефекта, реализуя алгоритм 3.3. При разработке программы использовались известные процедуры сортировки и поразрядного сравнения двоичных последовательностей.

4. Доказательство теорем в исчислении высказываний. Программа PROVE по исходной информации в виде секвенции, антецедентом (консеквентом) которой является входной набор, а консек-вентом (антецедентом) булева формула, описывающая диагностируемый фрагмент устройства, строит естественный логический вывод и решает вопрос, слу&ит ли такая секвенция теоремой. Укрупненная блок-схема программы построения естественного логического вывода представлена на рис. 4.2 и состоит из 7 блоков.

Едок I преобразует исходную секвенцию, заданную в скобочной форме, в польскую инверсную запись. При вводе информации в машину антецедент и консеквенг исходной секвенции долины быть заключены в отдельные скобки. Например " - машинное представление знака "V "). В формулах, вводимых в машину, не долішо быть вхождений подряд двух знаков " 1 ". Преобразование инсїюрмации процедурой P0LTZ производится посимвольно. Каждый текущий символ (ТС ) сравнивается с начальным массивом знаков " ( ", ") ", " [ ", " & в, " 1 ". Если ТС не знак (но и не пробел), то он поступает для формирования бесскобочного выражения; если ТС - пробел, то выполнение процедуры прекращается. Если ТС есть знак, но не " ) ", то при к = 0 (к - количество занятых ячеек в стеке) текущий ситлвол записывается в стек; при k 0 текущий символ сравнивается с помощью таблицы отношении (TGTN ) со знаком, записанным в ячейке стека с номером к . Б зависимости от значения отношения R текущий символ либо записывается в стек ( в = I ), либо выталкивает из стека (R =2) ранее записанные знаки в порядке очередности, начиная с последнего, которые поступают на формирование бесскобочного выражения.

Блок 2 исключения логических знаков из антецедента определяет тип последнего символа антецедента. Если это не " "I ", а " &, " или " 1 ", то знак, соответствующий последней операции при образовании антецедента или его формулы, исключается с помощью процедуры (блок 3) деления формул (процедура DXV ) и фигур заключения (2.3), (2.5). Полученные при этом одна или две - из посылки записываются в строки символов АМТ1 и ANT2. Если последним символом антецедента является буква, то в нем производится перегруппировка символов. Отделяется часть антецедента, начиная от конца, до первого встретившегося знака. Эта часть помещается в начало антецедента, а оставшаяся часть - в конец. Части разделяются запятой. Консеквент остается без изменения, формируется новая секвенция R&(k) , и программа возвращается к своему началу. Если в антецеденте нет знаков, то программа переходит к блоку 4 исключения логических знаков из консеквента. Если последним символом антецедента является знак " ", то весь антецедент или его часть, на которую действует этот знак, переносится без знака согласно фигуре заключения (2.7) в консеквент. Процедура деления формул (блок 3) работает следующим образом. Элементам таблицы, имеющей три строки и s/2 столбцов, где

S - количество символов в антецеденте (или консеквенте), присваиваются значения - I. Затем начинается замена этих значении в третьей строке таблицы значениями, вычисленными но формуле: P(3 N)= S + 3 + 1 , где N - номер столбца; 3 - номер текущего символа. Эта замена продолжается до тех пор, пока в формуле друг за другом, начиная с конца, следуют знаки " і " или " &, ". Если за знаками " \ " и " 8t " следует " 1 ", то заполнение третьей строки продолжается, а элементу второй строки и текущего столбца, присваивается нуль. Если же за знаками " 1 " и " & " следует буква, то элементу первой строки и текущего столбца присваивается значение I. Следующая текущая буква дает возможность присвоить значение I элементу второй строки и текущего столбца. Столбец, тлеющий все положительные элементы и наибольший номер, позволяет вычислить положительное значение элемента первой строки и столбца с номером на единицу меньшим, чем полностью заполненный.

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