Automatic Translation of Timed-Arc Petri Nets to Timed Automata
Student thesis: Master thesis (including HD thesis)
- Ye Tian
- Krishna Prasad Gundam
10. Term, Master Software Systems Engineering SSE
The main objective of this thesis is to investigate possibilities of
automatic verification of TAPN. We focus on translations of various
subclasses of TAPN into TA. Our aim is to verify the reachability
properties of TAPN by verifying the translated TA using verification
tool Uppaal.
Our reduction technique works for a sub-class of TAPN namely k-conservative nets. And the translator is implemented on Java platform considering both input and output files as XML files. Moreover we present two case studies on Fischer's protocol and Alternating Bit Protocol.
Our reduction technique works for a sub-class of TAPN namely k-conservative nets. And the translator is implemented on Java platform considering both input and output files as XML files. Moreover we present two case studies on Fischer's protocol and Alternating Bit Protocol.
Language | English |
---|---|
Publication date | Jun 2005 |