Preview

Информатика

Расширенный поиск

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

Аннотация

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

Об авторе

Д. И. Черемисинов
Объединенный институт проблем информатики НАН Беларуси
Беларусь


Рецензия

Для цитирования:


Черемисинов Д.И. ОБ ИНТЕРПРЕТАЦИИ ВРЕМЕННОЙ ЛОГИКИ ПРИ СИМВОЛИЧЕСКОЙ ВЕРИФИКАЦИИ. Информатика. 2004;(1(01)):132-138.

Просмотров: 437


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1816-0301 (Print)
ISSN 2617-6963 (Online)