Please wait a minute...
浙江大学学报(工学版)
J4  2011, Vol. 45 Issue (9): 1558-1565    DOI: 10.3785/j.issn.1008-973X.2011.09.008
计算机技术﹑电信技术     
基于符号模型检验的可信跨域协作系统验证方法
胡斌1,李阳1,高济2
1.杭州师范大学 杭州国际服务工程学院,浙江 杭州 310036；
2.浙江大学 计算机科学与技术学院,浙江 杭州 310027
Symbolic model checking based verification method
for trustworthy cross-organizational collaboration system
HU Bin1,LI Yang1,GAO Ji2
1.Hangzhou Institute of Service Engineering, Hangzhou Normal University, Hangzhou 310036, China;
2.College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China
 全文: PDF  HTML
摘要：

针对规范调控的可信跨域协作系统属性验证的困难,提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分.其中规范的状态语义是方案的核心,它将规范集映射为其所对应的状态或状态转移集,消除了系统模型和规范的语义不一致性；系统抽象模型包括规范Kripke结构和路径规范性定义,以及规范Kripke结构的分支时态逻辑（CTL）语义3个部分,实现了可信系统的形式建模；验证算法描述了系统符号模型检验的具体实现过程.与基于定理证明的验证方案相比,该方案有效降低了验证时间,提高了验证效率.
Abstract:

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．
出版日期: 2011-09-01
:  TP 182  
基金资助:

国家自然科学基金资助项目（61070153/F020701)，2010年浙江省优秀青年教师资助计划，浙江省教育厅资助项目（Y200805962）.
通讯作者: 高济，男，教授，博导.     E-mail: gaoji@hz.zj.cn
作者简介: 胡斌(1978-)，男，博士，讲师，主要从事形式验证、多Agent系统理论和技术的研究. E-mail: itenarent@yahoo.com.cn
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
作者相关文章　　

引用本文:

胡斌,李阳,高济. 基于符号模型检验的可信跨域协作系统验证方法[J]. J4, 2011, 45(9): 1558-1565.

HU Bin,LI Yang,GAO Ji. Symbolic model checking based verification method
for trustworthy cross-organizational collaboration system. J4, 2011, 45(9): 1558-1565.

链接本文:

https://www.zjujournals.com/eng/CN/10.3785/j.issn.1008-973X.2011.09.008    或    https://www.zjujournals.com/eng/CN/Y2011/V45/I9/1558

［1］ 高济, 吕何新, 郭航,等. 可信的自治式服务协调模型和应用开发框架［J］. 中国科学F辑: 信息科学, 2009, 39(11): 1146-1175．
GAO Ji, LV Hexin, GUO Hang. Trusted autonomic service cooperation model and application development framework ［J］. Science in China Series FInformation Sciences, 2009, 52(9): 1550-1577．
［2］ AGOTNES T, HOEK W V D, AGUILAR J A R, et al. On the logic of normative systems［C］∥ Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI 2007), Hyderabad, India ：AAAI,2007, 1175-1180．
［3］ ARTIKIS A, SERGOT M, PITT J. Specifying NormGoverned Computational Societies［J］. ACM Transactions on Computational Logic, 2008, 10(1): 1529-3785．
［4］ GOVERNATORI G, ROTOLO A. BIO logical agents: Norms, beliefs, intentions in defeasible logic［J］. Autonomous Agents and MultiAgent Systems, 2008, 17(1): 36-69．
［5］ SHOHAM Y, TENNENHOLTZ M. On social laws for artificial agent societies: offline design［J］. Artificial Intelligence, 1995, 73(1): 231-252．
［6］ BOMAN M. Norms in artificial decision making［J］. Artificial Intelligence and Law, 1999, 7(1): 7-35．
［7］ KROENING D, STRICHMAN O. Decision procedures: an algorithmic point of view［M］. Heidelberg: Springer, 2008．
［8］ CLARKE E M, GRUMBERG O, PELED D A. Model checking ［M］. London: The MIT Press, 1999．
［9］ HUTH M, RYAN M. Logic in computer science: modelling and reasoning about systems ［M］. Cambridge: Cambridge University Press, 2004．
［10］ BRYANT R E. Symbolic Boolean manipulation with ordered binarydecision diagrams ［J］. ACM Computing Survey, 1992, 24(3): 293-318．

［11］ TARSKI A. A latticetheoretical fixpoint theorem and its applications［J］. Pacific Journal of Mathematics, 1955, 5(2): 285-309．
［12］ 胡斌, 高济, 郭航. 规范多agent系统动态模型及其属性验证机制［J］. 浙江大学学报：工学版, 2009, 43 (6): 1014-1019,1167．
HU Bin, GAO Ji, GUO Hang. Dynamic model of normative multiagent system and its property verification mechanism ［J］. Journal of Zhejiang University ：Engineering Science, 2009, 43(6): 1014-1019,1167．
［13］ BRYANT R E. GraphBased Algorithms for boolean function manipulation［J］. IEEE Transactions on Computers, 1986, 35(8):677-691．
［14］ BAIER C, KATOEN J P. Principles of model checking［M］. Cambridge, MA, USA:The MIT Press, 2008．
［15］ SALCEDA J V. The role of norms and electronic institutions in multiagent systems applied to complex domains. The HARMONIA framework［D］. Catalonia： Technical University of Catalonia,2003．
［16］ VIRGINIA D. A Model for organizational interaction: based on agents, founded in logic ［D］. Utrecht, Netherlands:Utrecht University,2004．
[1] 徐萍, 高济, 郭航. 基于双层信誉和反馈机制的可信信誉计算[J]. J4, 2009, 43(12): 2160-2164.