Программирование для встроенных систем - статьи

       

Оракулы и спецификации


Оракулы – это процедуры, которые проверяют выполнение ограничений, наложенных на поведение целевой системы. В UniTesK оракулы полностью автоматически генерируются из описаний ограничений.

В UniTesK ограничения описываются преимущественно в форме имплицитных спецификаций стимулов и реакций. Кроме того, часть ограничений представляется в виде ограничений на значения типов (инварианты типов) и ограничений на значения глобальных переменных (инварианты глобальных переменных).



Содержание раздела