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 条
  • [11] Tarski A., A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5, 2, pp. 285-309, (1955)
  • [12] Hu B., Gao J., Guo H., Dynamic model of normative multi-agent system and its property verification mechanism, Journal of Zhejiang University: Engineering Science, 43, 6, (2009)
  • [13] Bryant R.E., Graph-Based Algorithms for boolean function manipulation, IEEE Transactions on Computers, 35, 8, pp. 677-691, (1986)
  • [14] Baier C., Katoen J.P., Principles of Model Checking, (2008)
  • [15] Salceda J.V., The role of norms and electronic institutions in multi-agent systems applied to complex domains. The HARMONIA framework, (2003)
  • [16] Virginia D., A Model for organizational interaction: Based on agents, founded in logic, (2004)
12