Проверка модели абстракции - Abstraction model checking

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

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

Галуа связан

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

То есть,

${displaystyle eta }$(${displaystyle heta }$(аннотация)) = аннотация
${displaystyle heta }$(${displaystyle eta }$(настоящий)) ${displaystyle supseteq }$ настоящий

Цикл уточнения абстракции

Проблема с абстракцией проверка модели состоит в том, что хотя абстракция имитирует реальную модель, когда абстракция не удовлетворяет какому-либо свойству, это не означает, что это свойство фактически не работает в реальной модели. Примеры счетчиков проверяются по реальному пространству состояний, потому что мы получаем «ложные» примеры счетчиков. Итак, часть цикла уточнения абстракции:

1. Получите абстрактную модель
2. Модель проверьте и посмотрите, все ли в порядке.
3. Если есть пример счетчика, вернитесь в реальное пространство состояний и выясните, действительно ли это модель счетчика.
4. Если нет, вернитесь и продолжите проверку модели.

Ложные примеры в основном генерируются из-за того, что тупиковые и плохие состояния абстрагируются до одного вида. Чтобы решить эту проблему, нам нужно создать разделение между двумя видами. Следующий шаг - найти подмножество невидимых переменных, которые действительно различают тупиковое и плохое состояния, и добавить это подмножество к набору видимых или наблюдаемых переменных. Если разделение окажется дорогостоящим, уточнение может быть основано на изучении образцов.

Рекомендации

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