• DocumentCode
    397850
  • 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
  • Volume
    3
  • fYear
    2003
  • fDate
    5-8 Oct. 2003
  • Firstpage
    2745
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Systems, Man and Cybernetics, 2003. IEEE International Conference on
  • ISSN
    1062-922X
  • Print_ISBN
    0-7803-7952-7
  • Type

    conf

  • DOI
    10.1109/ICSMC.2003.1244300
  • Filename
    1244300
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=397850