|
Эта публикация цитируется в 3 научных статьях (всего в 3 статьях)
Prosega/CPN: an extension of CPN Tools for automata-based analysis and system verification
[Prosega/CPN: расширение CPN Tools для автоматного анализа и верификации систем]
J. C. Carrasquela, A. Moralesb, M. E. Villapolc a La Sapienza University of Rome
b Central University of Venezuela
c Auckland University of Technology
Аннотация:
Верификация и анализ распределенных систем являются чрезвычайно важными задачами, особенно сейчас, когда многие компьютерные системы реализуют критически важные сервисы. Для моделирования и верификации систем полезно сочетать разные методы анализа. В частности, это позволяет применять тот формализм и ту технику анализа, которые лучше подходят для того или иного компонента системы. Комбинация из раскрашенных сетей Петри (CPN, Coloured Petri Nets) и конечных автоматов представляет собой успешную формальную методику моделирования и верификации распределенных систем. В связи с этим в данной статье рассматривается инструмент Prosega/CPN (Protocol Sequence Generator and Analyzer), расширение CPN Tools для поддержки автоматного анализа и верификации. Инструмент реализует несколько функций, таких как генерация минимизированного детерминированного конечного автомата из графа достижимости (occurrence graph) раскрашенной сети Петри, генерация языка и сопоставление конечных автоматов. Это решение поддерживается функцией Simulator Extensions, развитие которой обусловлено необходимостью интеграции раскрашенных сетей Петри с другими формализмами. Инструмент предназначен для поддержки формальной методологии верификации коммуникационных протоколов; однако он может использоваться для верификации других систем, анализ которых включает сравнение моделей на разных уровнях абстракции, например, бизнес-стратегий и бизнес-процессов. В статье приведен подробный пример, в котором инструмент Prosega/CPN используется для анализа части спецификации службы управления соединениями MAC IEEE 802.16.
Ключевые слова:
формальные методы, раскрашенные сети Петри, CPN Tools, конечные автоматы, верификация протоколов.
Образец цитирования:
J. C. Carrasquel, A. Morales, M. E. Villapol, “Prosega/CPN: an extension of CPN Tools for automata-based analysis and system verification”, Труды ИСП РАН, 30:4 (2018), 107–128
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tisp350 https://www.mathnet.ru/rus/tisp/v30/i4/p107
|
Статистика просмотров: |
Страница аннотации: | 209 | PDF полного текста: | 51 | Список литературы: | 21 |
|