大型复杂协议的形式化分析方法研究  

Methods for formal verification of large and complicated protocols

作　　者：赵娟[1] 韩继红[1] 王亚弟[1] 黄卿[1] 

机构地区：[1]信息工程大学电子技术学院,河南郑州450004

出　　处：《计算机工程与设计》2009年第18期4207-4210,共4页Computer Engineering and Design

摘　　要：大型复杂协议的形式化分析是目前研究的一个热点和难点。根据所采用技术的特点,将大型复杂协议的形式化分析方法分为基于逻辑推理的方法、基于模型检测的方法、基于定理证明的方法和基于进程代数的方法,并简要介绍了各类方法的代表性方法及验证器,最后对各类方法的特点进行分析和比较。指出达式大型复杂协议的形式化分析方法未来的一个研究重点,修改原有方法或设计一种新的方法,使其既易自动化实现,又能用于复合协议的分析和验证。The formal analysis of large and complicated protocols has been becoming a difficult hotspot of recent research. Based on the techniques used, the formal methods for analyzing large and complicated protocols are classified as logic reasoning based method, model checking based method, theorem proving based method and process algebra based method. The representative approaches and verifiers of each method are presented. At last, the characteristics of each approach are compared and the future research keystone for verifying large and complicated protocols is pointed out, namely amending original formal method or designing a new method to enable it to be automated easily and used for analysis of composed protocols.

关 键 词：大型复杂协议 形式化方法 逻辑推理 模型检测 定理证明 进程代数 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]