Automatic Translation of Timed-Arc Petri Nets to Timed Automata
Authors
Tian, Ye ; Gundam, Krishna Prasad
Term
10. Term
Education
Publication year
2005
Abstract
Denne afhandling undersøger automatisk verifikation af systemer modelleret med TAPN, et formelt værktøj til at beskrive adfærd med tidsaspekter. Vi oversætter flere underklasser af TAPN til TA, en relateret model som understøttes af verifikationsværktøjet Uppaal. Derefter kontrollerer vi nåbarhed (om bestemte tilstande kan nås) på de oversatte TA for at udlede de samme egenskaber for den oprindelige TAPN. Vores reduktionsteknik gælder for underklassen k‑konservative net. Oversætteren er implementeret i Java og bruger XML til ind- og uddata. Tilgangen illustreres med to casestudier: Fischers protokol og Alternating Bit Protocol.
This thesis explores automatic verification of systems modeled with TAPN, a formalism for describing behavior with timing. We translate several subclasses of TAPN into TA, a related model supported by the verification tool Uppaal. We then check reachability (whether certain states can be reached) on the translated TA to infer the same properties for the original TAPN. Our reduction technique applies to the TAPN subclass known as k-conservative nets. We implemented the translator in Java with XML input and output. The approach is illustrated with two case studies: Fischer's protocol and the Alternating Bit Protocol.
[This abstract was generated with the help of AI]
Documents