Model checking multilevel and recursive nets

Authors: Mirtha Lina Fernández Venero Flávio Soares Corrêa da Silva

Publish Date: 2016/01/02

Volume: 16, Issue: 4, Pages: 1117-1144

PDF Link

Abstract

With the increasing complexity of the problems and systems arising nowadays the use of multilevel 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 multilevel structure For instance several variants of multilevel Petri nets have been applied for modeling interaction protocols and mobility in multiagent systems and coordination of crossorganizational 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 multilevel 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 reachabilityWe are grateful to Gerard J Holzmann for his prompt replies to several questions concerning the use of process priorities in SPIN We also thank the anonymous reviewers for their comments and suggestions that helped to improve the presentation of this paper

Keywords: