ПОИСК Статьи Чертежи Таблицы Автоматизированная формулировка логических выводов из "Проектирование на ПЛИС архитектура, средства и методы " Главный недостаток системы SPIN заключается в том, что она изначально предназначена для проверки асинхронного программного обеспечения, то есть использует методы явной проверки. Хотя явная проверка идеально подходит для тестирования программных протоколов, эти методы могут оказаться неэффективными для больших аппаратных устройств. [c.323] Преимущество рассмотренного в предыдущем разделе метода верификации модели заключается в том, что этот процесс выполняется автоматически — нажимаем на кнопку и ждём результат. Однако вам, возможно, придётся довольно долго ждать окончания проверки. [c.323] Для автоматизированной формулировки не свойственны ограничения, присущие верификации моделей. Например, размеры системы не играют столь большого значения, так как автоматизированная формулировка не производит поиск пространства состояний. Кроме того, она подцерживает более высокий уровень выражений для точного моделирования сложных спецификаций. [c.324] К сожалению, то, что достигнуто в одних областях, уже утеряно в других. Несмотря на название, автоматизированная формулировка не выполняется в автоматическом режиме. На практике, при проверке устройства разработчики проводят доказательства с помощью определенных средств. Более того, для эффективного использования этих средств инженерам необходимо хорошо владеть стратегией доказательств, математической логикой и другими приёмами. Всё это требует нестандартных знаний, но если вы желаете потратить время и силы, то автоматизированная формулировка логических выводов, вероятно, будет наиболее мощным средством верификации ваших систем. [c.324] Вернуться к основной статье