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