| 基于xMAS模型的SpaceWire信誉逻辑的形式化验证 |
| |
| 引用本文： | 李艳春,李晓娟,关永,王瑞,张杰,魏洪兴.基于xMAS模型的SpaceWire信誉逻辑的形式化验证[J].计算机科学,2016,43(2):113-117, 134. |
| |
| 作者姓名： | 李艳春 李晓娟 关永 王瑞 张杰 魏洪兴 |
| |
| 作者单位： | 首都师范大学信息工程学院电子系统可靠性重点实验室 北京100048,首都师范大学信息工程学院电子系统可靠性重点实验室 北京100048,首都师范大学信息工程学院电子系统可靠性重点实验室 北京100048,首都师范大学信息工程学院电子系统可靠性重点实验室 北京100048,北京化工大学信息科学与技术学院 北京100029,北京航空航天大学机械工程及自动化学院 北京100191 |
| |
| 基金项目： | 本文受国际科技合作计划(2011DFG13000,2010DFB10930),国家自然科学基金项目(61373034,4,61379019),北京市教委科研基地建设项目(TJSHG201310028014),北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507),北京市教委(KM201510028015)资助 |
| |
| 摘 要： | 空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议, 保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。
|
| 关 键 词： | xMAS模型 信誉逻辑 SpaceWire 形式化验证 ACL2 |
| 收稿时间： | 2015/6/15 0:00:00 |
| 修稿时间： | 8/5/2015 12:00:00 AM |
xMAS-based Formal Verification of SpaceWire Credit Logic |
| |
| LI Yan-chun,LI Xiao-juan,GUAN Yong,WANG Rui,ZHANG Jie and WEI Hong-xing.xMAS-based Formal Verification of SpaceWire Credit Logic[J].Computer Science,2016,43(2):113-117, 134. |
| |
| Authors: | LI Yan-chun LI Xiao-juan GUAN Yong WANG Rui ZHANG Jie and WEI Hong-xing |
| |
| Affiliation: | Beijing Key Laboratory of Electronic System Reliability Technology,Information Engineering College, Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,Information Engineering College, Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,Information Engineering College, Capital Normal University,Beijing 100048,China,Beijing Key Laboratory of Electronic System Reliability Technology,Information Engineering College, Capital Normal University,Beijing 100048,China,College of Information Science & Technology,Beijing University of Chemical Technology,Beijing 100029,China and School of Mechanical Engineering and Automation,Beihang University,Beijing 100191,China |
| |
| Abstract: | SpaceWire protocol is a high-speed communication bus protocol applied to aerospace,so it is very important for communication system to ensure the reliability of the design.Due to the presence of a large number of queues,distributed control and concurrency,the traditional verification methods have incomplete defects and state explosion when model checking occurs.This paper presented a formal verification method of credit logic in SpaceWire communication system with xMAS model.xMAS model retains the structural information in lower level and can verify high-level attri-butes.The paper built an abstract xMAS model for credit logic and listed three key properties including sending,receiving and data consistency.Correctness of the properties was verified automatically by the ACL2 theorem proving tool.It can provide effective reference for system design under the guidance of verification. |
| |
| Keywords: | xMAS model Credit logic SpaceWire Formal verification ACL2 |
|
|
点击此处可从《计算机科学》下载全文 |
|
