文献检索-宁波市创意产业特色资源库

限定检索结果

基于xMAS模型的SpaceWire信誉逻辑的形式化验证: 收藏
分享
引用; 《计算机科学》2016年第2期43卷 113-117,134页; 作者：李艳春李晓娟关永王瑞张杰魏洪兴首都师范大学信息工程学院电子系统可靠性重点实验室北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191; 空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,...; 空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。; 来源：详细信息评论

高级检索 表达式检索

时间限定

文献类型

馆藏选择

核心期刊

语言

高级检索 表达式检索

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

限定检索结果

保存检索档案

请选择保存的检索档案：

收藏书架

请选择收藏分类：

检索条件订阅

申请转借

引用

高级检索 表达式检索

时间限定

文献类型

馆藏选择

核心期刊

语言

高级检索 表达式检索

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

限定检索结果

保存检索档案

请选择保存的检索档案： 新增检索档案 确定 取消

收藏书架

请选择收藏分类： 新增自定义分类 确定 取消

检索条件订阅

申请转借

引用

高级检索表达式检索

高级检索表达式检索

请选择保存的检索档案：

请选择收藏分类：