Computer Science – Software Engineering
Scientific paper
2011-07-06
Computer Science
Software Engineering
8 pages, submitted to conference for publication
Scientific paper
We introduce a technique for reachability analysis of Time-Basic (TB) Petri nets, a powerful formalism for real- time systems where time constraints are expressed as intervals, representing possible transition firing times, whose bounds are functions of marking's time description. The technique consists of building a symbolic reachability graph relying on a sort of time coverage, and overcomes the limitations of the only available analyzer for TB nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. The graph construction algorithm has been automated by a tool-set, briefly described in the paper together with its main functionality and analysis capability. A running example is used throughout the paper to sketch the symbolic graph construction. A use case describing a small real system - that the running example is an excerpt from - has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper. Ongoing work, in the perspective of integrating with a model-checking engine, is shortly discussed.
Bellettini Carlo
Capra Lorenzo
No associations
LandOfFree
Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-678669