摘要
针对规范调控的可信跨域协作系统属性验证的困难,提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分.其中规范的状态语义是方案的核心,它将规范集映射为其所对应的状态或状态转移集,消除了系统模型和规范的语义不一致性;系统抽象模型包括规范Kripke结构和路径规范性定义,以及规范Kripke结构的分支时态逻辑(CTL)语义3个部分,实现了可信系统的形式建模;验证算法描述了系统符号模型检验的具体实现过程.与基于定理证明的验证方案相比,该方案有效降低了验证时间,提高了验证效率.
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.
出处
《浙江大学学报（工学版）》
EI
CAS
CSCD
北大核心
2011年第9期1558-1565,1635,共9页
Journal of Zhejiang University：Engineering Science
基金
国家自然科学基金资助项目(61070153/F020701)
2010年浙江省优秀青年教师资助计划
浙江省教育厅资助项目(Y200805962)
关键词
形式验证
符号模型检验
跨域协作
formal verification
symbolic model checking
cross-organizational collaboration
