ИМПЛИКАЦИЯ И ЭКВИВАЛЕНТНОСТЬ КАК ОСНОВА ВЕРИФИКАЦИИ
КРАТКИЕ СООБЩЕНИЯ
УДК 004.056.53 ИМПЛИКАЦИЯ И ЭКВИВАЛЕНТНОСТЬ КАК ОСНОВА ВЕРИФИКАЦИИ О.Ф. Немолочнов, А.Г. Зыков, В.И. Поляков
Рассматривается использование функций импликации и эквивалентности при верификации логических схем и программного продукта в процессе их проектирования и реализации. Ключевые слова: проектирование, верификация, импликация, эквивалентность, вычислительный процесс.
Повышающиеся требования к качеству аппаратно-программных комплексов заставляют разработчиков уделять все большее внимание вопросам тестирования и верификации разрабатываемых изделий. Поэтому разработка моделей и эффективных методов анализа схем и программ является актуальной проблемой. К методам анализа аппаратуры и программных продуктов в первую очередь относятся верификация и тестирование.
При проектировании любого вычислительного процесса в виде логической схемы или программы всегда имеется два объекта, которые необходимо верифицировать: A – задание на проект (техническое задание или спецификация проекта) и B – реализация проекта (в виде логической схемы или программы).
При рассмотрении процесса проектирования между объектами A и B должно соблюдаться следующее соотношение: A B, т.е. A должно содержаться в B. Отсюда следует, что A→B. Соответственно, A есть достаточный, а B – необходимый признаки. Полная эквивалентность A≡B может быть выдержана только в том случае, если A→B и B→A, что, как правило, недостижимо [1].
Отношение A B возникает из-за различного характера допущений при конкретной реализации проекта и является характерным при использовании стандартных решений – заготовок, например, при использовании полузаказного проектирования для схем или CASE-технологий при программировании.
Основой верификации вычислительных процессов является переход к формализации функций импликации и эквивалентности на основе результатов вычислений. Сложность верификации вычислительных процессов, особенно в больших проектах, возникает из-за наличия ситуаций don’t care и недекларированных возможностей в проектах, которые необходимо обнаружить и локализовать [2]. Учет указанных ситуаций позволяет верифицировать исследуемые объекты с большей достоверностью и дает возможность диагностировать вычислительный процесс на возможность вирусного проникновения (заражения).
Особое место при верификации вычислительных процессов занимает верификация управляющих вычислительных систем, особенность которых заключается в том, что они работают в синхронизированном режиме, определяемом объектом управления. В этом случае может возникнуть явление состязаний сигналов, в том числе и критических, которые в обязательном порядке должны быть выявлены и устранены [3]. С другой стороны, появляется задача привязки асинхронных сигналов к вычислительному – управляющему процессу. Это приводит к появлению ждущих вершин и, соответственно, к приостановке вычислительного процесса и введению в него задержек, асинхронных по своей природе. Разрешение указанных противоречий необходимо проводить путем введения в вычислительный процесс синхросигналов с калиброванным по частоте расстоянием между ними, что и должно обеспечивать качество и, в конечном итоге, достоверность верификаций управляющих процессов.
Таким образом, импликация и эквивалентность (с учетом ситуаций don’t care и недекларированных возможностей, а также синхронизации в управляющих вычислительных процессах) являются основой верификации вычислительных процессов.
1. Импликация и неопределенные значения условий-предикатов вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Поляков В.И. // Труды Международных научно-технических конференций «Интеллектуальные системы» (AIS’08) и «Интеллектуальные САПР» (CAD-2008), Научное издание в 4-х томах. – М.: Физматлит, 2008. – Т. 1. – 400 с. – С. 140–145.
2. Метод обнаружения недекларированных возможностей и DON’T CARE вычислительного процесса / Немолочнов О.Ф., Зыков А.Г., Кулагин В.С., Осовецкий Л.Г., Поляков В.И., Суханов А.В. // Известия вузов. Приборостроение. – 2009. – Т. 52. – № 12. – С. 32–39.
3. Анализ и устранение критических состязаний сигналов при синтезе тестовых последовательностей / Немолочнов О.Ф. // А и Т. – 1976. – № 11.
Немолочнов Олег Фомич – СПбГУ ИТМО, доктор технических наук, профессор, зав. кафедрой, nemolochnov_o_f@mail.ru; Зыков Анатолий Геннадьевич – СПбГУ ИТМО, кандидат технических наук, доцент, zykov_a_g@mail.ru; Поляков Владимир Иванович – СПбГУ ИТМО, кандидат технических наук, доцент, v_i_polyakov@mail.ru
122
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2010, № 4(68)
УДК 004.056.53 ИМПЛИКАЦИЯ И ЭКВИВАЛЕНТНОСТЬ КАК ОСНОВА ВЕРИФИКАЦИИ О.Ф. Немолочнов, А.Г. Зыков, В.И. Поляков
Рассматривается использование функций импликации и эквивалентности при верификации логических схем и программного продукта в процессе их проектирования и реализации. Ключевые слова: проектирование, верификация, импликация, эквивалентность, вычислительный процесс.
Повышающиеся требования к качеству аппаратно-программных комплексов заставляют разработчиков уделять все большее внимание вопросам тестирования и верификации разрабатываемых изделий. Поэтому разработка моделей и эффективных методов анализа схем и программ является актуальной проблемой. К методам анализа аппаратуры и программных продуктов в первую очередь относятся верификация и тестирование.
При проектировании любого вычислительного процесса в виде логической схемы или программы всегда имеется два объекта, которые необходимо верифицировать: A – задание на проект (техническое задание или спецификация проекта) и B – реализация проекта (в виде логической схемы или программы).
При рассмотрении процесса проектирования между объектами A и B должно соблюдаться следующее соотношение: A B, т.е. A должно содержаться в B. Отсюда следует, что A→B. Соответственно, A есть достаточный, а B – необходимый признаки. Полная эквивалентность A≡B может быть выдержана только в том случае, если A→B и B→A, что, как правило, недостижимо [1].
Отношение A B возникает из-за различного характера допущений при конкретной реализации проекта и является характерным при использовании стандартных решений – заготовок, например, при использовании полузаказного проектирования для схем или CASE-технологий при программировании.
Основой верификации вычислительных процессов является переход к формализации функций импликации и эквивалентности на основе результатов вычислений. Сложность верификации вычислительных процессов, особенно в больших проектах, возникает из-за наличия ситуаций don’t care и недекларированных возможностей в проектах, которые необходимо обнаружить и локализовать [2]. Учет указанных ситуаций позволяет верифицировать исследуемые объекты с большей достоверностью и дает возможность диагностировать вычислительный процесс на возможность вирусного проникновения (заражения).
Особое место при верификации вычислительных процессов занимает верификация управляющих вычислительных систем, особенность которых заключается в том, что они работают в синхронизированном режиме, определяемом объектом управления. В этом случае может возникнуть явление состязаний сигналов, в том числе и критических, которые в обязательном порядке должны быть выявлены и устранены [3]. С другой стороны, появляется задача привязки асинхронных сигналов к вычислительному – управляющему процессу. Это приводит к появлению ждущих вершин и, соответственно, к приостановке вычислительного процесса и введению в него задержек, асинхронных по своей природе. Разрешение указанных противоречий необходимо проводить путем введения в вычислительный процесс синхросигналов с калиброванным по частоте расстоянием между ними, что и должно обеспечивать качество и, в конечном итоге, достоверность верификаций управляющих процессов.
Таким образом, импликация и эквивалентность (с учетом ситуаций don’t care и недекларированных возможностей, а также синхронизации в управляющих вычислительных процессах) являются основой верификации вычислительных процессов.
1. Импликация и неопределенные значения условий-предикатов вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Поляков В.И. // Труды Международных научно-технических конференций «Интеллектуальные системы» (AIS’08) и «Интеллектуальные САПР» (CAD-2008), Научное издание в 4-х томах. – М.: Физматлит, 2008. – Т. 1. – 400 с. – С. 140–145.
2. Метод обнаружения недекларированных возможностей и DON’T CARE вычислительного процесса / Немолочнов О.Ф., Зыков А.Г., Кулагин В.С., Осовецкий Л.Г., Поляков В.И., Суханов А.В. // Известия вузов. Приборостроение. – 2009. – Т. 52. – № 12. – С. 32–39.
3. Анализ и устранение критических состязаний сигналов при синтезе тестовых последовательностей / Немолочнов О.Ф. // А и Т. – 1976. – № 11.
Немолочнов Олег Фомич – СПбГУ ИТМО, доктор технических наук, профессор, зав. кафедрой, nemolochnov_o_f@mail.ru; Зыков Анатолий Геннадьевич – СПбГУ ИТМО, кандидат технических наук, доцент, zykov_a_g@mail.ru; Поляков Владимир Иванович – СПбГУ ИТМО, кандидат технических наук, доцент, v_i_polyakov@mail.ru
122
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2010, № 4(68)