раздел 2.3):
?(11)min [?s / s(11), ?s / s(11), ?s / s(11)] = min [k+1/1, k+1/1,k+1/1] = k+1. Это свойство означает, что в телефонной сети может одновременно происходить не более k+1 телефонных разговоров.
Повторяемость или L3-живость. СП обладает свойством повторяемости (или L3-живости), поскольку все переходы покрываются ненулевыми координатами из минимального порождающего множества Т-инвариантов:
t = (1,0,1,0,0,0,0,0,0,0,0,0), t = (0,0,0,0,0,0,0,0,0,0,1,1), t = (1,1,0,1,1,0,0,0,0,0,0,0),
t = (1,1,0,0,0,1,0,0,0,1,0,0), t = (0,1,0,0,0,1,1,1,0,0,0,0), t = (1,1,0,0,0,1,1,0,1,0,0,1).
Физическая интерпретация этого свойства означает, что в телефонной сети повторное соединение любых двух абонентов возможно практически бесконечное число раз.
Непротиворечивость. СП обладает свойством непротиворечивости, поскольку любая разметка ? является достижимой из самой себя. Это значит, что телефонная сеть всегда приходит в исходное состояние.
СП является консервативной, тот есть в случае наличия каналов и абонентов число фишек в СП всегда равно .
Данная СП не является контролируемой, так как ранг её матрицы инцидентности меньше количества мест в СП.
Взаимное исключение в данной СП состоит в том, что никакой телефон не может быть одновременно в состоянии занят и свободен. Это свойство имеет место, т.к. разметки и не являются достижимыми в этой СП. Этот факт следует из решения уравнения состояния для данных разметок.
Кроме того, согласно доказанной выше теореме 9, данное динамическое свойство следует из того факта, что существуют не равные нулю произведения вектора свободных членов уравнения состояния данной СП и полученных S-инвариантов, что означает несовместность данного уравнения состояния. Тогда из несовместности уравнения состояния следует недостижимость разметки, отражающей одновременной нахождение абонента в состоянии "занят" и "свободен", из заданной начальной.
Действительно, пусть начальная разметка СП , а разметка, соответствующая проверяемому состоянию одновременного пребывания телефона в состоянии "занят" и "свободен" (а также ). Тогда . Рассмотрим произведения всех семи S-инвариантов на . Получим, что произведения и первого, четвёртого, пятого, шестого и седьмого S-инвариантов не равны нулю. Рассмотрим также и произведения всех семи S-инвариантов на . Получим, что произведения и третьего, пятого и седьмого S-инвариантов не равны нулю.
Доказать данное свойство взаимного исключения можно также с помощью S-инвариантов, рассматривая минимальное порождающее множество, соответствующее местам, которые моделируют взаимоисключающие состояния системы.
Таким образом, в результате проведенного анализа можно сделать вывод, что построенная формальная модель имеет требуемые зафиксированные свойства данной реальной системы, и данный набор MSC-диаграмм корректно описывает модель POTS. Напомним, что в процессе перевода из MSC в СП формируется таблица, которая служит для поддержания постоянной связи между описанием системы в языке MSC и её представлением в виде сети Петри. С помощью этой таблицы найденные проблемы и ошибки системы могут представляться инженеру-разработчику в формате MSC-диаграмм.
4.2 Свойства процесса
Подводя итог, отметим, что главными свойствами данного технологического процесса являются следующие: во-первых, процесс автоматизированный, во-вторых, входной язык и язык выходных вердиктов являются рабочими языкам инженеров-разработчиков и, следовательно, не требуют специальной математической подготовки. Кроме того, выделим следующие дополнительные свойства.
Практичность и эффективность. Применение данного процесса гарантирует определенные преимущества в сравнении с ранее использовавшимися методами и средствами, а также экономит время пользователя. Данный технологический процесс является основой построения чекера. Как следует из литературы, современный мировой опыт отмечает большую эффективность применения чекеров по сравнению с пруверами для верификации и анализа проектируемых систем.
Открытая система. Новые функциональные возможности могут наращиваться с целью удовлетворения потребностей проектировщиков, обеспечиая все более удобную адаптацию к имеющимся средствам или более удобное средство написания спецификаций.
Многоцелевое и интегрированное использование. Реализация технологического процесса является относительно дешёвой и предназначается для многих пользователей. Например, существует возможность его применения к единичной спецификации в некоторых точках программы при анализе в процессе проектирования, при оптимизации кода, при генерации тестов и при тестировании. Чекер, построенный на основе данного процесса, может работать вместе с другими программными методами и средствами, в среде объединенной общими языками (или языком) программирования. Кроме того, его использование может интегрироваться с традиционными средствами программного проектирования, такими как компиляторы и симуляторы.
Легкость в использовании и обучении. Данное свойство непосредственно следует из второго главного свойства процесса. А именно, простота в использовании следует из того, что входные и выходные данные привычны для понимания инженера-разработчика. Кроме того, проектировщик или пользователь должен обладать минимумом знаний для того, чтобы применять данный технологический процесс.
Ориентация на определенный класс ошибок. Данный процесс может быть настроен на поиск заданного класса ошибок, сохраняя при этом корректность анализируемого изделия. Он также поддерживает процесс генерации тестов для отладки системы.
Поддержка эволюционного проектирования систем. Процесс поддерживает эволюционное проектирование системы посредством частичных спецификаций и анализа выбранных свойств системы. В частности, процесс даёт возможность концентрироваться на одном единственном свойстве системы, например, на анализе определенного свойства в потоке сообщений протокола.
Трудность конкретной реализации данного технол