A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems

摘要: In cooperative systems (CSs), participants cannot usually ensure the correct behavior of their partners. Obligations and proofs have to be performed together achieve a common goal in real cooperation. Without adequate accountability assurances actions, there is no means reliably enforcing punitive measures against fraudulent participants. However, existing formal methods for analyzing CSs properly deal with obligations. As such, this paper proposes new class labeled Petri net (LPN) models. The each partner represented by an LPN, while CS modeled combination all partners' LPN behavioral properties overall system can well verified only individual LPN. LPNs provide integration notations graphical commonly used verification techniques. obligations are based on languages nonblocking action sequences, proved network conditions local sequences partner's side. proposed approaches illustrated modeling analysis purchase transaction using Internet Open Trading Protocol.