ОБ ИНТЕРПРЕТАЦИИ ВРЕМЕННОЙ ЛОГИКИ ПРИ СИМВОЛИЧЕСКОЙ ВЕРИФИКАЦИИ

Abstract

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