Model checking multi-level and recursive nets
| Autor: | Flávio Soares Corrêa da Silva, Mirtha Lina Fernández Venero |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Class (computer programming) Theoretical computer science Computer science Distributed computing 020207 software engineering 02 engineering and technology Petri net Process architecture Promela Reachability Modeling and Simulation ENGENHARIA DE SOFTWARE 0202 electrical engineering electronic engineering information engineering Stochastic Petri net SPIN model checker 020201 artificial intelligence & image processing computer Software computer.programming_language |
| Zdroj: | Repositório Institucional da USP (Biblioteca Digital da Produção Intelectual) Universidade de São Paulo (USP) instacron:USP |
| ISSN: | 1619-1374 1619-1366 |
| DOI: | 10.1007/s10270-015-0509-6 |
| Popis: | With the increasing complexity of the problems and systems arising nowadays, the use of multi-level models is becoming more frequent in practice. However, there are still few reports in the literature concerning methods for analyzing such models without flattening the multi-level structure. For instance, several variants of multi-level Petri nets have been applied for modeling interaction protocols and mobility in multi-agent systems and coordination of cross-organizational workflows. But there are few automated tools for analyzing the behavior of these nets. In this paper we explain how to detect faults in models based on a representative class of multi-level nets: the nested Petri nets. We translate a nested net into a verifiable model that preserves its modular structure, a PROMELA program. This allows the use of SPIN model checker to verify properties related to termination, boundedness and reachability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink