国家高技术研究发展计划(8633010503)

作品数：4被引量：13H指数：2
导出分析报告
相关作者：张德运董皓陈海诠肖健宇傅鹏更多>>
相关机构：西安交通大学更多>>
相关期刊：《微电子学与计算机》《计算机工程》更多>>
相关主题：B方法形式化方法UML状态机形式化规约程序依赖图更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种改进的并发程序静态切片算法被引量：3
《计算机工程》2006年第14期14-16,45,共4页肖健宇 张德运 陈海诠 董皓 
国家"863"计划基金(8633010503)
分析了Krinke切片算法对循环体内嵌套有线程的程序结构会产生切片不精确的现象,认为其原因是该算法对线程间数据依赖的定义过于粗糙,且对程序行为约束不够。该文提出一种新算法,在并发程序内部表示中,增加跨线程边界循环-承载数据依赖,...
关键词：静态程序切片 并发程序 切片算法 程序依赖图 执行证据 
基于形式语言B的一种新的时态规约方案被引量：1
《微电子学与计算机》2006年第2期16-19,共4页肖健宇 张德运 陈海诠 董皓 
国家863计划项目(8633010503)
提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证。该方案中,时间类型表示为B方法中系统内部支持的非负整数集合,所有依赖于时间的变量都表示成定义域为时间的全函数。该方案可以方便地表达...
关键词：时态规约 形式化方法 实时系统 B方法 B函数 
基于后缀树词序列核挖掘Web文档被引量：2
《微电子学与计算机》2005年第12期4-7,共4页傅鹏 张德运 陈海诠 董皓 
国家863计划项目(8633010503)
通过将文档表示为一棵后缀树,文章提出一种基于后缀树索引计算文档相似度的词序列核。首先根据文档的词序列构造出后缀树,然后根据后缀树词序列核计算文档间的相似度,最后利用支持向量机对文档进行分类。理论分析表明后缀树词序列核的...
关键词：核学习方法 词序列核 字符串核 后缀树 WEB挖掘 
UML状态机到B形式化规约的转换被引量：7
《微电子学与计算机》2005年第8期80-84,共5页肖健宇 张德运 董皓 陈海诠 
国家863网络安全管理与测评技术(8633010503)
文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则,涵...
关键词：UML状态机 形式化方法 B方法 高可信软件工程 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部