Автоматизированная верификация счетчиковых систем посредством предметно-ориентированной многорезультатной суперкомпиляции
Аннотация:
Рассматривается применение суперкомпиляции к анализу поведения счетчиковых систем переходов. Многорезультатная суперкомпиляция позволяет обнаруживать наилучшие варианты анализа, благодаря тому, что порождается множество возможных результатов анализа, которое затем фильтруется в
соответствии с некоторыми критериями. К сожалению, пространство поиска при этом может получаться весьма обширным. Однако, можно значительно уменьшить объем поиска за счет учета особенностей предметной области.
Таким образом, сочетание предметно-ориентированной и многорезультатной суперкомпиляции может давать синергетический эффект. Затраты на реализацию предметно-ориентированных многорезультатных суперкомпиляторов могут быть невелики, если использовать компоненты, предоставляемые инструментарием MRSC.
Язык публикации: русский/английский,
страниц:30/28
