A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems
A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems
复制标题
DOI：
10.1109/tsmca.2008.2010751
复制
发表时间：
2009-03
期刊：
影响因子：
--
通讯作者：
Yuyue Du;Changjun Jiang;Mengchu Zhou
中科院分区：
文献类型：
--
作者：
Yuyue Du;Changjun Jiang;Mengchu Zhou
在合作系统（CS）中，参与者通常不能确保他们的合作伙伴的正确行为。参与者的义务和证明必须共同履行，以实现真实的合作中的共同目标。如果没有对行动的充分问责保证，就没有办法对欺诈性参与者可靠地执行惩罚措施。然而，现有的正式的方法来分析CS不能妥善处理问责制和义务。因此，本文提出了一类新的标记Petri网（LPN）模型。每个合作伙伴的行为由一个LPN表示，而CS由所有合作伙伴的LPN模型的组合来建模。只有通过分析每个单独的LPN，才能很好地验证整个建模系统的行为特性。LPN提供了形式符号与图形符号以及形式证明与常用验证技术的集成。的义务进行验证的基础上的LPN语言和非阻塞性能的动作序列，而问责制可以证明网络条件和本地的动作序列在每个合作伙伴的一方。所提出的方法说明了使用互联网开放交易协议的购买交易的建模和分析。
In cooperative systems (CSs), participants cannot usually ensure the correct behavior of their partners. Obligations and proofs of participants have to be performed together to achieve a common goal in a real cooperation. Without adequate accountability assurances of actions, there is no means of reliably enforcing punitive measures against fraudulent participants. However, the existing formal methods for analyzing CSs cannot properly deal with accountability and obligations. As such, this paper proposes a new class of labeled Petri net (LPN) models. The behavior of each partner is represented by an LPN, while a CS is modeled by the combination of all partners' LPN models. The behavioral properties of an overall modeled system can be well verified only by analyzing each individual LPN. LPNs provide the integration of formal notations with graphical notations and formal proofs with commonly used verification techniques. The obligations are verified based on LPN languages and the nonblocking properties of action sequences, while accountability can be proved by the network conditions and local action sequences on each partner's side. The proposed approaches are illustrated with the modeling and analysis of a purchase transaction using the Internet Open Trading Protocol.