基于xMAS模型的SpaceWire信誉逻辑的形式化验证

• 作者: 关永 张杰 李晓娟 李艳春 王瑞 魏洪兴
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: xMAS模型 信誉逻辑 SpaceWire 形式化验证 ACL2
• 年，卷（期）: 2016,（2）
• 所属期刊栏目: 网络与通信
• 页码范围: 113-117,134
• 页数: 6页
• 分类号: TP311
• 字数: 6785字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.2.026

摘要

空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要.但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题.基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性.对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证.该方法为验证指导下的系统设计提供了有效的参考.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	关永	首都师范大学信息工程学院电子系统可靠性重点实验室	95	1336	17.0	33.0
3	李晓娟	首都师范大学信息工程学院电子系统可靠性重点实验室	39	261	9.0	14.0
4	魏洪兴	北京航空航天大学机械工程及自动化学院	86	1477	19.0	36.0
5	王瑞	首都师范大学信息工程学院电子系统可靠性重点实验室	10	44	4.0	6.0
6	李艳春	首都师范大学信息工程学院电子系统可靠性重点实验室	2	4	1.0	2.0