作者：闫靖晨; 程京德安全性规格ccz时序逻辑形式化验证方法
摘要：随着信息系统在社会生活中越来越重要,越来越必不可缺,人们对信息系统的安全性需求也不断地增加.不允许出现安全性漏洞的非常重要的信息系统,其安全性规格必须要使用形式化方法来描述且验证才是可靠的.介绍了在世界上首先提出的基于国际通用标准CC（ISO/IEC15408）的安全性规格描述及验证方法.把国际通用标准CC中定义的功能元素作为信息安全性评价标准,用形式化规格描述语言Z和时序逻辑来进行形式化描述.另一方面,用UML把保护轮廓PP模式化,并在用Z形式化地描述了目标信息系统的安全性规格之后,采用定理证明方法和模型检测方法来对目标系统的安全性规格进行形式化验证.为了让只具备基础知识的验证者也能够轻松使用该方法,开发了其支援工具FORVEST.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
