Title :
Deadlock-free verification of RosettaNet PIPs with time Petri nets
Author :
Da-Yin Liao ; Liu, Paladin R.
Author_Institution :
Dept. of Inf. Manage., Nat. Chi-Nan Univ., Nantou, Taiwan
Abstract :
This paper deals with the verification problem of RosettaNet. The RosettaNet PIPs specifications are first modelled with time Petri nets (TPNs) which allow an explicit modelling of concurrency and parallelism. We demonstrate that RosettaNet PIPs are deadlock-free in both the deterministic and stochastic operational environments. A patch subnet technique is developed to improve the efficiency of RosettaNet PIPs. We also suggest to remove some steps defined in RosettaNet PIPs that are proved to never take place.
Keywords :
Petri nets; concurrency theory; electronic commerce; formal specification; formal verification; parallel processing; protocols; Rosettanet partner interface process; business transactions; communication protocols; deadlock free verification; patch subnet technique; time petri nets; Collaboration; Concurrent computing; Electronics industry; Information management; Petri nets; Protocols; Resumes; Stochastic processes; System recovery; System testing;
Conference_Titel :
Systems, Man and Cybernetics, 2003. IEEE International Conference on
Print_ISBN :
0-7803-7952-7
DOI :
10.1109/ICSMC.2003.1244300
