任龙涛

作品数：5被引量：30H指数：2
导出分析报告
供职机构：大连理工大学国家示范性软件学院更多>>
发文主题：形式化验证STM嵌入式软件迁移矩阵级联故障更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《计算机工程与设计》《计算机科学》更多>>
所获基金：国家自然科学基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于时间自动机的嵌入式软件压缩与验证被引量：1
《计算机工程与设计》2016年第5期1217-1223,共7页任龙涛 张超 崔磊 魏理豪 周宽久 
利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条件符号化状态压缩法,对自动机模型进行压缩;在此基础上提出一...
关键词：时间自动机 模型验证 嵌入式软件 状态空间压缩 可满足性模理论 
基于时间Petri网的嵌入式系统中断建模与验证
《计算机科学》2014年第9期205-209,219,共6页周宽久 常军旺 侯刚 任龙涛 王小龙 
国家自然科学基金:航天多核嵌入式软件可信性验证与系统原型(61272174)资助
嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上...
关键词：中断建模 有界模型检测 时间自动机 可满足性模理论 时间PETRI网 
基于层次化时间STM软件设计的形式化验证被引量：1
《计算机科学》2014年第8期42-46,共5页周宽久 任龙涛 王小龙 勇嘉伟 侯刚 
国家自然科学基金(61272174)资助
状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这...
关键词：层次化时间状态迁移矩阵 形式化验证 有界模型检测 
软件动态执行网络建模及其级联故障分析被引量：3
《计算机科学》2014年第8期109-114,共6页王小龙 侯刚 任龙涛 周宽久 常军旺 王竹 
国家自然科学基金(61272174)资助
随着人们对软件功能需求的不断增加,软件系统的结构和规模越来越复杂。如何对复杂软件系统的拓扑结构及其质量进行有效分析和评估是软件工程中亟待解决的难题。采用复杂网络理论对软件系统进行建模和求解,将软件源代码中的函数作为节点...
关键词：复杂网络 软件执行路径 加权拓扑网络 CML模型 级联故障 
模型检测中状态爆炸问题研究综述被引量：25
《计算机科学》2013年第06A期77-86,111,共11页侯刚 周宽久 勇嘉伟 任龙涛 王小龙 
国家自然科学基金项目(91018003;61272174)资助
模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述...
关键词：软件系统 模型检测 状态空间爆炸 形式化验证 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部