ОБ ИНТЕРПРЕТАЦИИ ВРЕМЕННОЙ ЛОГИКИ ПРИ СИМВОЛИЧЕСКОЙ ВЕРИФИКАЦИИ
В последние годы инструменты для символической верификации на основе временной логики входят в состав большинства индустриальных САПР СБИС. В символических верификаторах используется логика ветвящегося времени CTL. Ее недостатком считается неинтуитивность. Предлагаются интерпретации временных логик,...
| Format: | Article |
|---|---|
| Language: | Russian |
| Published: |
The United Institute of Informatics Problems of the National Academy of Sciences of Belarus
2019-02-01
|
| Series: | Informatika |
| Online Access: | https://inf.grid.by/jour/article/view/813 |
| Summary: | В последние годы инструменты для символической верификации на основе временной логики входят в состав большинства индустриальных САПР СБИС. В символических верификаторах используется логика ветвящегося времени CTL. Ее недостатком считается неинтуитивность. Предлагаются интерпретации временных логик, в которых выразительность и интуитивность CTL для интервальных событий не хуже, чем выразительность и интуитивность LTL для мгновенных событий, что позволяет упростить формулирование проверяемых временных свойств. |
|---|---|
| ISSN: | 1816-0301 |