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

• Автор: Галин, Александр Борисович
• Шифр специальности: 05.13.01
• Научная степень: Кандидатская
• Год защиты: 1984
• Место защиты: Ростов-на-Дону
• Количество страниц: 147 c. : ил

ВВЕДЕНИЕ
1. АНАЛИЗ СОВРЕМЕННЫХ МЕТОДОВ ДИАГНОСТИРОВАНИЯ ЦИФРОВЫХ УСТРОЙСТВ И ПРОГРАММНЫХ СРЕДСТВ.

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

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

1.3. Выводы
2. ДИАГНОСТИРОВАНИЕ КОМБИНАЦИОННЫХ УСТРОЙСТВ НА ОСНОВЕ ЕСТЕСТВЕННОГО ЛОГИЧЕСКОГО ВЫВОДА

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

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

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

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

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

формул
2.6. Проверка правильности программ, реализующих
булевы функции
2.6.1. Сходство и различие между задачами диагностирования аппаратуры и программных средств
2.6.2. Методика проверки правильности программ,реализующих булевы функции
2.7. Выводы .
3. ДИАГНОСТИРОВАНИЕ УПРАВЛЯЮЩИХ ЛОГИЧЕСКИХ УСТРОЙСТВ
НА ОСНОВЕ СПЕЦИАЛЬНОГО ПРЕДСТАВЛЕНИЯ ИХ СТРУКТУРЫ
3.1. Модель управляющего логического устройства.
3.1.1. Модель управляющей части логического устройства
3.1.2. Алгоритмы построения последовательностей управляющих воздействий записи и считывания информации
3.2. Проверка исправности путей передачи инфорлации и совокупностей элементов памяти управляющей
части логического устройства
3.3. Алгоритм проверки исправности управляющего логического устройства
3.4. Алгоритм идентификации представленной модификации управляющего логического устройства .
3.5. Выводы
4. РАЗРАБОТКА И ИССЛЕДОВАНИЕ АВТОМТИЗИРОВАННОЙ СИСТЕМЫ
ДИАГНОСТИРОВАНИЯ УПРАВЛЯЩИХ ЛОГИЧЕСКИХ УСТРОЙСТВ.
4.1. Блок сопряжения диагностируемого объекта с ЭВМ
4.2. Организация и описание комплекса прикладных программ системы диагностирования .
4.3. Результаты использования автоматизированной системы для диагностирования управляющего логического устройства .
4.4. Выводы .
ЗАКЛЮЧЕНИЕ .
ЛИТЕРАТУРА


В работе на основе специального представления структуры объекта, структурно-аналитического описания его на языке булевых функций и применения машинных методов доказательства теорем в исчислении высказываний решены задачи проверки спецификации и диагностирования управляющих логических устройств. Внедрение результатов работы позволяет проверять правильность программ, реализующих булевы функции, и выполнять проверку исправности и поиск логических дефектов в комбинационных схемах и управляющих логических устройствах на этапе проектирования без трудоемкой и дорогостоящей процедуры предварительного построения тестов. Реализация работы. Результаты диссертации использованы в хоздоговорных работах, выполненных на кафедре прикладной математики и вычислительной техники Е1СИ № / (ГР К , инв. Л№ 2, 3) и / (ГР # 0), а также в работе по госбюджетной тематике "Математическое обеспечение САПР" (ГР , инв. Разработанные методы и алгоритмы использованы при диагностировании управляющих логических устройств, при проверке правильности программ и, в частности, программы микропроцессорного устройства управления специальным технологическим процессом, при разработке автоматизированной системы диагностирования УЛУ. Ожидаемый экономический эффект от использования материалов работы составит тыс. Способы диагностирования одновыходных комбинационных автоматов и управляющих логических устройств. Алгоритмы проверки исправности и идентификации представленной модификации одновыходного комбинационного устройства общего вида и управляющего логического устройства. Методика проверки правильности программ, реализующих булевы функции. Способ реализации автоматизированной системы диагностирования управляющих логических устройств. Материалы диссертационной работы распределены по разделам следующим образом. В первом разделе изложены результаты анализа современного состояния проблемы диагностирования ЦУ. Рассмотрены ставшие уже "классическими" методы, применяемые при производстве и эксплуатации ЦУ, - аппаратные, программные и программно-аппаратные, а также методы проектирования контролепригодных устройств: специализированные, применяемые при создании конкретного ЦУ или системы, и структурные, решающие проблему диагностирования в общем случае. В этом разделе такае рассматриваются основные методы диагностирования программных средств. Анализируются некоторые методы проверки правильности программ на этапе проектирования. Констатируется, что поскольку теоретических основ предмета пока не существует, часто используются эмпирические правила при проверке программ. При этом установлено, что некоторые методы диагностирования аппаратных средств могут быть перенесены в соответствующей интерпретации на программные средства. Второй раздел посвящен диагностированию комбинационных автоматов и проверке правильности программ, реализующих булевы функции, на основе естественного логического вывода. Предлагаются два алгоритма автоматического диагностирования комбинационного устройства без предварительного построения тестов, основанные на применении машинного доказательства теорем в исчислении высказываний. Первый алгоритм - проверки исправности - предполагает известной только структурно-аналитическую форлулу исправного устройства, заданную в скобочном виде. Второй - идентификации представленной модификации - предполагает заданными структурно-аналитическую формулу исправного устройства и список формул неисправных модификаций, соответствующий перечню логических дефектов объекта. С помощью стратегии направленного перебора входных воздействий и эксперимента над объектом определяется его техническое состояние, а поиск дефекта осуществляется путем идентификации одной из формул заданного списка Приводятся оценки слок-ности разработанных алгоритмов. Примеры диагностирования комбинационных устройств подтверждают эффективность предложенного метода. Методика проверки правильности программ, реализующих булевы функции, разработана на основе алгоритма проверки исправности комбинационного автомата. Эффективность методики подтверкдается на примере проверки программы микропроцессорного управляющего.