Проверка абстрактной модели

В информатике и математике проверка абстрактной модели — это форма проверки модели для систем, в которых фактическое представление слишком сложно для разработки одной модели. Таким образом, дизайн подвергается своего рода переводу в уменьшенную «абстрактную» версию.

Множество переменных разделяется на видимые и невидимые в зависимости от изменения их значений. Реальное пространство состояний сводится к меньшему набору видимых состояний.

Галуа на связи

Реальное и абстрактное пространства состояний связаны Галуа . Это означает, что если мы возьмем элемент из абстрактного пространства, конкретизируем его и абстрагируем конкретизированную версию, то результат будет равен оригиналу. С другой стороны, если вы выберете элемент из реального пространства, абстрагируете его и конкретизируете абстрактную версию, конечным результатом будет супермножество оригинала.

То есть,

$\eta$( $\theta$(абстрактный)) = абстрактный
$\theta$( $\eta$(настоящий)) $\supseteq$ настоящий

См. также

• Абстрактная интерпретация
• Автоматизированное доказательство теорем
• Логика дерева вычислений
• Формальная проверка
• Список инструментов проверки модели
• Программный анализ (информатика)
• Статический анализ кода

Ссылки

• Эдмунд М. Кларк, Орна Грумберг и Дэвид Э. Лонг (1994). «Проверка модели и абстракция». Транзакции ACM в языках и системах программирования . 16 (5): 1512–1542. CiteSeerX   10.1.1.79.3022 . дои : 10.1145/186025.186051 . S2CID   207884170 .