国家教育部博士点基金(200807010012)

作品数：8被引量：35H指数：4
导出分析报告
相关作者：段振华田聪张琛门鹏王小兵更多>>
相关机构：西安电子科技大学武汉大学更多>>
相关期刊：《西安交通大学学报》《光子学报》《西安电子科技大学学报》《计算机研究与发展》更多>>
相关主题：命题投影时序逻辑时序逻辑WEB服务组合形式化验证模型检测工具更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于事件确定有限自动机的UML2.0序列图描述与验证被引量：8
《软件学报》2011年第11期2625-2638,共14页张琛 段振华 田聪 
国家自然科学基金(60433010;60873018;60910004;91018010;61003078;61003079;61133001);国家重点基础研究发展计划(973)(2010CB328102);国家教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004)
为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata...
关键词：UML2.0序列图 事件确定有限自动机 模型检测 命题投影时序逻辑 验证 
BPEL流程建模中的交叠模式分析与转换被引量：5
《软件学报》2011年第11期2684-2697,共14页张曼 段振华 王小兵 
国家自然科学基金(60910004;60873018;91018010;61003078;61003079;61133001);国家重点基础研究发展计划(973)(2010CB328102);国家教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004);综合业务网国家重点实验室基金(201102001)
由图形化流程建模语言生成可执行的业务流程语言(business process execution language,简称BPEL)时,对于源模型中顺序与并发结构交织的情况(称为交叠模式),传统的复制相关活动方法缺少系统分析及形式化描述.针对这一现状,提出基于工作...
关键词：BPEL 商业流程建模 自由选择工作流网 合成规则 交叠模式 
应用UML2.0模型的测试用例生成方法被引量：8
《西安交通大学学报》2011年第8期18-23,共6页张琛 段振华 
国家重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(60433010;60873018;60910004;91018010;61003078;61003079);教育部高等学校博士学科点专项科研基金资助项目(200807010012);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证...
关键词：测试用例 命题投影时序逻辑 模型检测 覆盖准则 
基于命题投影时序逻辑的单调速率调度算法模型检测被引量：3
《软件学报》2011年第2期211-221,共11页田聪 段振华 
国家自然科学基金(61003078;91018010;60873018;60910004);国家重点基础研究发展计划(973)(2010CB328102);教育部博士点基金(200807010012);中央高校基本科研业务费专项资金(JY10000903004)
提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系...
关键词：时序逻辑 模型检测 单调速率调度算法 验证 实时系统 
Einstein谜的SAT求解被引量：4
《计算机科学》2010年第5期184-186,共3页田聪 段振华 王小兵 
国家自然科学基金重点基金项目(60433010);国家自然科学基金项目(60373103;60873018);总装115预研项目(51315050105);教育部博士点基金(200807010012);软件工程国家重点实验室(SKLSE20080713)资助
Einstein谜,亦称Zebra谜,是爱因斯坦在20世纪初提出的,他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题,可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求解问题,并使用当前流行的SAT求解器,如MinSat,对Einstein...
关键词：Einstein谜 命题逻辑 可满足性 验证 形式化方法 
着色Petri网模型检测工具的扩展及其在Web服务组合中的应用被引量：8
《计算机研究与发展》2009年第8期1294-1303,共10页门鹏 段振华 
国家自然科学基金项目(60433010;60873018);教育部高等学校博士学科点基金项目(200807010012)~~
Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模...
关键词：着色PETRI网 WEB服务组合 形式化验证 模型检测 时序逻辑 
区间时序逻辑的模型检查被引量：2
《西安电子科技大学学报》2009年第2期338-342,共5页张海宾 段振华 
国家自然科学基金资助(60873018;60871097);国家自然科学基金重大项目资助(60433010);博士点基金资助(200807010012)
为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规...
关键词：模型检查 时序逻辑 自动机 
动态Web服务组合的选择策略
《光子学报》2009年第2期325-328,共4页门鹏 段振华 
国家自然科学基金(60433010;60873018);装备预先研究项目(51315050105);博士点基金(200807010012)资助
为了提高光网络资源的利用率,提出一种基于Petri网的Web服务组合最优化选择的方法.根据用户需求使用Petri网对服务组合之间的数据依赖关系建模,利用Petri网的T-不变量得到各种可能组合方案,并对于每种组合方案使用广义随机Petri网分析...
关键词：WEB服务组合 PETRI网 光网络 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部