Symbolic model checking based verification method for trustworthy cross-organizational collaboration system

被引：0
|
作者：
Hu B. [1 ]
Li Y. [1 ]
Gao J. [2 ]
机构：
[1] Hangzhou Institute of Service Engineering, Hangzhou Normal University
[2] College of Computer Science and Technology, Zhejiang University
来源：
Zhejiang Daxue Xuebao (Gongxue Ban)/Journal of Zhejiang University (Engineering Science) | 2011年 / 45卷 / 09期
关键词：
Cross-organizational collaboration; Formal verification; Symbolic model checking;
D O I：
10.3785/j.issn.1008-973X.2011.09.008
中图分类号：
学科分类号：
摘要：
Towards the difficulty of property verification in the norm-governed trustworthy cross-organizational collaboration system, this work introduced a verification method based on symbolic model checking. This method includes three different parts: the syntax and semantics of norms, the abstract system model and the verification algorithm. The semantics of norms constitute the core of the whole method. It maps norms into the state sets or the state transition sets that satisfy them, thus eliminates the semantics gap between norms and the system model. The abstract model, which includes the definition of normative Kripke structure, normative traces, and the computation tree logic (CTL) semantics under the system model, provides the framework for formally modeling the collaboration systems. The verification algorithm is the implementation of the method. In contrast to the theorem-proven based verification, this method can effectively reduce the verification time, thus improve the verification efficiency.
引用
收藏
页码：1558 / 1565+1635
相关论文
共 16 条
  • [1] Gao J., Lv H.-X., Guo H., Trusted autonomic service cooperation model and application development framework, Science in China Series F-Information Sciences, 52, 9, pp. 1550-1577, (2009)
  • [2] Agotnes T., Hoek W.V.D., Aguilar J.A.R., Et al., On the logic of normative systems, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 1175-1180, (2007)
  • [3] Artikis A., Sergot M., Pitt J., Specifying norm-governed computational societies, ACM Transactions on Computational Logic, 10, 1, pp. 1529-3785, (2008)
  • [4] Governatori G., Rotolo A., BIO logical agents: Norms, beliefs, intentions in defeasible logic, Autonomous Agents and Multi-Agent Systems, 17, 1, pp. 36-69, (2008)
  • [5] Shoham Y., Tennenholtz M., On social laws for artificial agent societies: Off-line design, Artificial Intelligence, 73, 1, pp. 231-252, (1995)
  • [6] Boman M., Norms in artificial decision making, Artificial Intelligence and Law, 7, 1, pp. 7-35, (1999)
  • [7] Kroening D., Strichman O., Decision Procedures: An Algorithmic Point of View, (2008)
  • [8] Clarke E.M., Grumberg O., Peled D.A., Model Checking, (1999)
  • [9] Huth M., Ryan M., Logic in Computer Science: Modelling and Reasoning about Systems, (2004)
  • [10] Bryant R.E., Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Survey, 24, 3, pp. 293-318, (1992)
12