Абстрактное состояние
Абстрактное состояние – это множество структур данных, которые моделируют внутреннее состояние целевой системы. Все действия, которые выполняет целевая система, моделируются в терминах абстрактного состояния.
Документация на IPv6 не содержит требований к внутреннему устройству реализации IPv6. Абстрактное состояние было спроектировано таким образом, чтобы предоставить удобные концептуальные структуры данных для спецификаций стимулов и реакций.
Абстрактное состояние для MSR IPv6 включает следующие элементы:
- Множество исходящих пакетов IPv6. Это множество моделирует множество пакетов, которые реализация передает канальному уровню
- Набор очередей входящих датаграм UDP. Данные очереди используются для моделирования получения данных клиентами UDP.
- Пул фрагментов. Пул фрагментов используется для двух целей. (1) мы моделируем процедуру сборки пакетов в целевой системе. (2) мы проверяем, что из фрагментов, которые выпускает целевая система, получатель сможет воссоздать оригинальный пакет
- Набор таблиц Neighbor Discovery. Эти таблицы используются при моделировании алгоритмов Neighbor Discovery.