| Avalon片上总线协议的形式化建模与模型检验分析 |
| |
| 引用本文： | 谭华,古天龙.Avalon片上总线协议的形式化建模与模型检验分析[J].桂林电子科技大学学报,2009,29(2). |
| |
| 作者姓名： | 谭华 古天龙 |
| |
| 作者单位： | 桂林电子科技大学计算机与控制学院,广西桂林,541004 |
| |
| 摘 要： | 片上总线协议是片上总线技术的核心,其设计的好坏直接影响到片上系统芯片的可靠性.针对Avalon片上总线协议的自身特点和复杂性,给出了Avalon总线协议的一种有限状态饥分析模型,并用CTL对协议的相关属性进行形式化描述,同时采用模型检验工具SMV进行验证分析,验证结果表明协议不存在安全漏洞.
|
| 关 键 词： | 片上总线 Avalon总线协议 有限状态机 计算树逻辑 模型检验 |
Formal Modeling and Model Checking Analysis of the Avalon System-on-Chip Bus Protocol |
| |
| TAN Hua,GU Tian-long.Formal Modeling and Model Checking Analysis of the Avalon System-on-Chip Bus Protocol[J].Journal of Guilin Institute of Electronic Technology,2009,29(2). |
| |
| Authors: | TAN Hua GU Tian-long |
| |
| Affiliation: | School of Computer Science and Control Technology;Guilin University of Electronic Technology;Guilin 541004;China |
| |
| Abstract: | In Bus-based on-chip system(SOC),kinds of IP cores are interconnected by On-chip-bus(OCB) and the data interactive is to comply with the bus protocol.As a core technology in SOC,the chip bus protocol greatly determines reliability in SOC.The characteristic and complexity bring great challenge for formal analysis and verification.In this paper,the Avalon Onchip-bus was used as an example,and an efficient way for formal analysis of the system on a programmable bus protocol was developed.Firstly,the informatio... |
| |
| Keywords: | on-chip-bus Avalon bus protocol finite state machine computation tree logic model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
