符号模型检验

作品数：29被引量：55H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：董荣胜古天龙郭云川刘建元罗莉更多>>
相关机构：北京交通大学桂林电子工业学院国防科学技术大学西安邮电学院更多>>
相关期刊：《兰州理工大学学报》《电子科技文摘》《陕西师范大学学报（自然科学版）》《铁道通信信号》更多>>
相关基金：国家自然科学基金广西省自然科学基金广西壮族自治区自然科学基金国家重点实验室开放基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
ARINC653实时任务可调度性验证方法被引量：1
《单片机与嵌入式系统应用》2021年第4期15-20,共6页雷煜靓 胡宁 陈福 崔西宁 
国防基础科研项目资助(JCKY2016607B006);工信部民机科研(MJ-2017-S-39)。
针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方...
关键词：ARINC653 可调度性 秒表时间自动机 统计模型检验 符号模型检验 
应答器报文编制规则的形式化建模与验证被引量：6
《铁道学报》2019年第6期100-106,共7页黄旭 刘中田 
中央高校基本科研业务费(2017JBM009)
应答器报文的正确与否直接关系到列车运行安全。CTCS-2级列控系统应答器的应用原则是C2应答器报文编制的起点和依据,应答器报文的正确性与应用原则的正确性及其是否被正确执行直接相关。基于文本语言描述的应答器应用原则易产生二义性问...
关键词：应答器报文 应答器应用原则 符号模型检验 UML 
问题框架中问题领域因果行为的形式化验证被引量：1
《计算机科学》2015年第12期136-142,156,共8页朱利鲁 李智 
国家自然科学基金(61262004;61262005);广西自然科学基金(2012GXNSFCA053010);广西科学研究与技术开发计划项目(桂科合1347004-22);广西教育厅科研项目(201203YB023);广西多源信息挖掘与安全重点实验室开放基金(14-A-03-01);"八桂学者"工程专项经费资助
为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号...
关键词：问题框架 关键问题领域 因果行为 符号模型检验 可达性 
基于Craig插值的线性混成系统符号化模型检测被引量：2
《电子学报》2014年第7期1338-1346,共9页陈祖希 徐中伟 霍伟伟 喻钢 
国家自然科学基金(No.60674004;No.61075002;No.71302048);十二五国家科技支撑计划(No.2011BAG01B03);国家863高技术研究发展计划(No.2012AA112801);铁道部重点研究发展计划(No.2012AA112801)
最强后件的计算是模型检测算法的核心.本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式,利用一阶逻辑公式不可满足情况下的插值存在性定理,对线性混成自动机的有界模型检测公式进行指定的划分,使用支...
关键词：Craig插值 可满足性模理论 线性混成自动机 符号模型检验 混成系统 
CTCS-2级列控系统的形式化建模与验证被引量：1
《计算机工程》2013年第3期12-15,共4页董昱 水晶 黎磊 
国家自然科学基金资助项目(61164010);甘肃省教育厅硕导基金资助项目(210110)
由于CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使...
关键词：列控系统 符号模型检验 形式化方法 车载设备 模式转换 
网络协议的形式化分析与设计
《科技资讯》2013年第8期34-35,共2页徐文超 
随着形式化方法和技术的日趋完善,网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础,渗透到网络协议分析、综合、测试等各环节的软件工程方法。本文从网络协议的基本要素、协议的形式化模型介绍了网络协...
关键词：网络协议 形式化分析 符号模型检验 
异步FIFO的模型检验方法被引量：1
《计算机科学》2012年第3期268-270,共3页罗莉 欧国东 刘彬 徐炜遐 窦强 
核高基重大专项(2011ZX01028-001-001)资助
跨时钟域(Clock Domain Crossing,CDC)设计和验证是SOC系统芯片设计的关键问题。讨论了异步FIFO的模型检验方法,利用模型检验工具SMV,建立了异步FIFO的有限状态机模型,使用时序逻辑LTL对该模型和属性进行了描述和验证。实验结果达到要求...
关键词：CDC(Clock Domain Crossing) 异步FIFO LTL 符号模型检验 SMV 
基于符号模型检验的可信跨域协作系统验证方法
《浙江大学学报（工学版）》2011年第9期1558-1565,1635,共9页胡斌 李阳 高济 
国家自然科学基金资助项目(61070153/F020701);2010年浙江省优秀青年教师资助计划;浙江省教育厅资助项目(Y200805962)
针对规范调控的可信跨域协作系统属性验证的困难,提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分.其中规范的状态语义是方案的核心,它将规范集映射为其所对应的...
关键词：形式验证 符号模型检验 跨域协作 
基于UML的CTCS-3级列控系统需求规范形式化验证方法被引量：10
《中国铁道科学》2011年第3期93-99,共7页刘金涛 唐涛 徐田华 赵林 
国家自然基金重点资助项目(60634010);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)
采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证。使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象。根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相...
关键词：列车控制系统 需求规范 形式化方法 UML 符号模型检验 
基于UML的建模及模型检验研究被引量：3
《现代电子技术》2011年第6期49-51,54,共4页吴晓丹 宁滨 
UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UML模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建...
关键词：UML 符号模型检验 SMV 模型转换 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部