Verification of Reachability Problems for Time Basic Petri Nets
This addresses verification challenges for real-time systems modeled with Time-Basic Petri nets, representing an incremental improvement over prior methods.
The paper tackles the problem of verifying reachability in Time-Basic Petri nets, a formalism for real-time systems, by introducing a technique that constructs a finite symbolic reachability graph to overcome limitations of existing analyzers, with the method automated in a Java tool-set and benchmarked on a real-world example.
Time-Basic Petri nets, is a powerful formalism for model- ing real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for reachability analysis based on the building of finite contraction of the infinite state space associated with such a models. The technique constructs a finite symbolic reachability graph relying on a sort of time coverage, and over- comes the limitations of the existing available analyzers for Time-Basic nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. A key feature of the technique is the introduction of the Time Anonymous concept, which allows the identification of components not influencing the evolution of a model. A running example is used throughout the paper to sketch the symbolic graph construction. The graph construction algorithm has been automated by a Java tool-set, described in the paper together with its main functionality and analysis capability. A use case describing a real-world example has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper.