Верификационная система
Cтраница 1
Верификационная система ВЕРСИЯ имеет встроенный диалог, позволяющий пользователю упростить с ней работу. [1]
Хотя в ИК реализована специальная верификационная система ВЕРСИЯ, анализ протоколов начинается уже на этапе обработки спецификации протокольным препроцессором ( см. гл. Такой анализ назовем раздельным анализом, так как он выполняется без учета взаимодействий с другими протокольными объектами. Входные данные, полученные в результате работы протокольного препроцессора, используются системой ВЕРСИЯ уже для анализа взаимодействий протокольных объектов друг с другом, который поэтому назовем совместным. [2]
При построении дерева глобальных состояний верификационная система обнаружит совпадающие состояния, находящиеся на одном пути из корня ( исходное и состояние В), которые указывают на два цикла ( на рисунке обозначены пунктирными стрелками): первый характеризует повторные попытки записи при получении пользователем отрицательных подтверждений, а второй - повторные попытки чтения. Так как оба цикла являются полезными и имеют выход, разработчик, проанализировав информацию, выданную верификационной системой, не будет вносить эти циклы к динамической блокировке. [3]
 |
Средства обработки спецификаций. [4] |
И, наконец, система ВЕРСИЯ представляет собой интерактивную верификационную систему для анализа формальных описаний протоколов, работа которой основана на хорошо известном методе анализа дерева достижимых состояний. [5]
Анализ спецификации транспортного протокола был выполнен на верификационной системе ВЕРСИЯ ( см. гл. [6]
Данное начальное состояние является корнем дерева достижимых глобальных состояний, построенного верификационной системой ВЕРСИЯ. [7]
И последний этап анализа ( шаг III) заключается в том, что на вход верификационной системы поступают полные спецификации N - и N - объектов, по которым строится глобальное дерево достижимых состояний. [8]
 |
Часть базы данных БДАРХ. [9] |
К программным средствам для автоматической обработки спецификаций относятся протокольный препроцессор вместе с системой САГА, протокольный комплексатор и верификационная система ВЕРСИЯ. [10]
Основой верификационной системы ВЕРСИЯ является метод построения дерева достижимых состояний. Используемый метод анализа такого дерева является развитием метода [52], который в настоящее время наиболее широко используется для анализа протоколов. [11]
При построении дерева глобальных состояний верификационная система обнаружит совпадающие состояния, находящиеся на одном пути из корня ( исходное и состояние В), которые указывают на два цикла ( на рисунке обозначены пунктирными стрелками): первый характеризует повторные попытки записи при получении пользователем отрицательных подтверждений, а второй - повторные попытки чтения. Так как оба цикла являются полезными и имеют выход, разработчик, проанализировав информацию, выданную верификационной системой, не будет вносить эти циклы к динамической блокировке. [12]
Страницы: 1