国家自然科学基金(60433010)

作品数：28被引量：175H指数：5
导出分析报告
相关作者：段振华王小兵雷丽晖张海宾舒新峰更多>>
相关机构：西安电子科技大学西北大学武汉大学西安交通大学更多>>
相关期刊：《计算机技术与发展》《西安电子科技大学学报》《西北大学学报（自然科学版）》《西安交通大学学报》更多>>
相关主题：投影时序逻辑时序逻辑形式化验证组合WEB服务区间时序逻辑更多>>
相关领域：自动化与计算机技术理学更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于主动网络的自适应VPN体系结构
《信息技术》2012年第7期29-30,35,共3页刘旭勇 
国家自然科学基金项目(60433010);陕西省科技攻关项目(2009K08-11)
主动网络为网络节点和在网络中传输的分组增加了可编程能力,使得网络成为了一个动态的自适应网络。简述了VPN协议和方案所面临的挑战,提出了基于主动网络的自适应的VPN体系结构,该结构能够提供灵活的便携式服务,并且能在动态环境下提供...
关键词：主动网络 可编程 VPN 
投影时序逻辑在系统建模中的应用被引量：1
《西北大学学报（自然科学版）》2010年第3期410-414,共5页舒新峰 段振华 
国家自然科学基金资助项目(60873018);国家自然科学基金重点基金资助项目(60433010)
目的为了解决形式化验证时需要分别使用不同工具进行系统建模和性质描述的问题。方法利用投影时序逻辑PTL(projection temporal logic)在同一逻辑框架内完成待验证系统的建模和性质的描述。结果对PTL投影操作符的特点和用途进行了详细分...
关键词：投影时序逻辑 系统建模 形式化验证 
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谜 命题逻辑 可满足性 验证 形式化方法 
利用投影时序逻辑的多内核进程调度建模与验证被引量：2
《西安交通大学学报》2010年第3期52-57,共6页舒新峰 段振华 
国家自然科学基金资助重大国际合作项目(60910004);国家"973计划"重点资助项目(2010CB328102);国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);总装备部预研项目(51315050105)
针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公...
关键词：投影时序逻辑 进程调度 定理证明 多核处理器 调度验证 
MSVL语言的公理系统的程序验证
《西安电子科技大学学报》2010年第1期96-101,共6页杨潇潇 段振华 
国家自然科学基金资助项目(60873018);国家自然科学基金重点资助项目(60433010)
MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区...
关键词：形式验证 时序逻辑 正则形 安全性 公理系统 
时序逻辑程序的模型检测被引量：4
《计算机科学》2009年第10期164-167,共4页王小兵 段振华 
国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金项目(SKLSE20080713)资助
时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序p和性质Ф统一表示在投影时序逻辑中...
关键词：时序逻辑程序 形式化验证 正则图 模型检测 
投影时序逻辑的公理系统与形式验证被引量：4
《西安电子科技大学学报》2009年第4期680-685,729,共7页舒新峰 段振华 
国家自然科学基金资助(60873018);国家自然科学基金重点项目资助(60433010)
为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统.利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,...
关键词：投影时序逻辑 公理系统 形式化方法 验证 
良基归纳法在时序逻辑程序不变式验证中的应用被引量：1
《计算机科学》2009年第6期150-152,共3页杨潇潇 段振华 
国家自然科学基金资助项目(60873018);国家自然科学基金重大资助项目(60433010)资助
并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所...
关键词：时序逻辑程序 正则形 良基关系 良基归纳法 不变式证明 
面向投影时序逻辑的Web服务模型检测被引量：5
《西安交通大学学报》2009年第4期39-43,124,共6页王小兵 段振华 
国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713)
为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定...
关键词：形式逻辑 投影时序逻辑 WEB服务 模型检测 
区间时序逻辑的模型检查被引量：2
《西安电子科技大学学报》2009年第2期338-342,共5页张海宾 段振华 
国家自然科学基金资助(60873018;60871097);国家自然科学基金重大项目资助(60433010);博士点基金资助(200807010012)
为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规...
关键词：模型检查 时序逻辑 自动机 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部