中央高校基本科研业务费专项资金(JY10000903004)

作品数：10被引量：30H指数：3
导出分析报告
相关作者：段振华杨琛张琛田聪王小兵更多>>
相关机构：西安电子科技大学武汉大学西安邮电学院更多>>
相关期刊：《西安电子科技大学学报》《兰州大学学报（自然科学版）》《西安交通大学学报》《软件学报》更多>>
相关主题：命题投影时序逻辑时序逻辑测试用例生成方法测试用例UML2.0更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一个轻量的多核实时调度算法
《兰州大学学报（自然科学版）》2012年第5期118-123,共6页聂鹏程 
国家自然科学基金青年基金项目(61003079);陕西省工业攻关计划项目(2009K01-36);中央高校基本科研业务费专项项目(JY10000903004)
为了解决现有多核实时调度算法要么利用率界限低、要么开销大的问题,在k分组的半局部最早时限优先算法的基础上提出了一个轻量的多核实时调度算法PsEKG.该算法引入一种周期敏感的机制,在任务分配之前先将周期成倍数关系的任务组织在一起...
关键词：多核 实时 调度 
工作流网合成规则及其在流程设计中的应用被引量：1
《西安电子科技大学学报》2012年第2期200-206,共7页张曼 段振华 
国家自然科学基金资助项目(60910004,60873018,91018010,61003078,61003079,61133001);国家重点基础研究发展计划(973)资助项目(2010CB328102);综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对工作流网建模过程中节点精化方法只能扩展单节点的局限性,提出一种基于Petri网合成规则的工作流网精化方法.在活的和有界的自由选择网合成规则上添加限制,使其适用于自由选择工作流网的精化,定义可分离工作流网及其保持可分离性的...
关键词：工作流 PETRI网 合成规则 自由选择工作流网 可分离工作流网 
基于事件确定有限自动机的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序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证...
关键词：测试用例 命题投影时序逻辑 模型检测 覆盖准则 
支持Stutter-不变性的命题区间时序逻辑
《西安电子科技大学学报》2011年第2期151-156,共6页杨琛 段振华 
国家自然科学基金重大国际合作项目资助项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展计划(973)资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项基金资助项目(JY10000903004)
为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,...
关键词：模型检测 时序逻辑 状态爆炸 
有穷时间投影时序逻辑的完备公理系统被引量：5
《软件学报》2011年第3期366-380,共15页舒新峰 段振华 
国家自然科学基金(60433010;60910004;60873018;91018010;61003078;61003079);国家重点基础研究发展计划(973)(2010CB328102);中央高校基本科研业务费专项资金(JY10000903004)
为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称...
关键词：投影时序逻辑 公理系统 完备性证明 定理证明 形式化方法 
基于命题投影时序逻辑的单调速率调度算法模型检测被引量：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描述系...
关键词：时序逻辑 模型检测 单调速率调度算法 验证 实时系统 
PPTL模型检测器实现的一个关键技术被引量：3
《西安交通大学学报》2010年第10期24-29,共6页杨琛 段振华 
国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,...
关键词：时序逻辑 自动机 模型检测 
面向命题投影时序逻辑的安全协议模型检测被引量：1
《西安交通大学学报》2010年第8期30-35,共6页杨琛 段振华 王小兵 
国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望...
关键词：模型检测 协议验证 时序逻辑 安全协议 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部