区间时序逻辑

作品数：15被引量：26H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：段振华张海宾周清雷朱维军雷丽晖更多>>
相关机构：西安电子科技大学郑州大学汕头大学华南理工大学更多>>
相关期刊：《计算机与数字工程》《计算机学报》《郑州大学学报（理学版）》《西安电子科技大学学报》更多>>
相关基金：国家自然科学基金国家教育部博士点基金国家高技术研究发展计划中国博士后科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于有穷论域下区间时序逻辑的模型检测研究被引量：1
《计算机与数字工程》2018年第7期1302-1305,1451,共5页李超 
通过结合自动机技术实现了有穷论域区间时序逻辑的判定算法,给出了有穷论域下区间时序逻辑变量、函数的处理方法,并提出了利用自动机进行系统建模的方法。最终实现了一个基于有穷论域区间时序逻辑的模型检测工具。
关键词：区间时序逻辑 模型检测 自动机 
基于时序逻辑的3种网络攻击建模被引量：5
《计算机科学》2018年第2期209-214,共6页聂凯 周清雷 朱维军 张朝阳 
国家重点研发计划(2016YFB0800100);国家自然科学基金(U1204608;U1304606;61572444);中国博士后科学基金(2015M572120;2012M511588)资助
与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式,该方法不能检测出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签...
关键词：命题区间时序逻辑 实时攻击签名逻辑 模型检测 入侵检测 
具有程序的静态结构和动态行为语义的时序逻辑
《计算机研究与发展》2016年第9期2067-2084,共18页陈冬火 刘全 金海东 朱斐 王辉 
国家自然科学基金项目(61272005;61303108;61373094;61472262;61502323;61502329);江苏省自然科学基金项目(BK2012616);福建省自然科学基金项目(2014J01221);江苏省高校自然科学研究项目(13KJB520020);吉林大学符号计算与知识工程教育部重点实验室项目(93K172014K04);苏州市应用基础研究计划项目(SYG201422)~~
提出一种区间分支时序逻辑——控制流区间时序逻辑(control flow interval temporal logic,CFITL),用于规约程序的时序属性.不同于计算树逻辑(computation tree logic,CTL)和线性时序逻辑(linear temporal logic,LTL)等传统的时序逻辑,C...
关键词：区间时序逻辑 控制流程图 程序静态结构 模型检验 可满足性模理论 
基于时间区间时序逻辑的实时系统统一模型检测
《电子科技大学学报》2014年第5期712-716,共5页朱维军 乔芃喆 周清雷 张海宾 
国家自然科学基金(U1204608;U1304606;61373043);中国博士后科学基金(2012M511588)
在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型...
关键词：统一模型检测 实时系统 可满足性判定 时间区间时序逻辑 
扩展Tempura语言统一模型检测算法
《华南理工大学学报（自然科学版）》2011年第7期163-168,共6页朱维军 周清雷 张海宾 
国家"863"计划项目(2007AA010408);国家自然科学基金青年基金资助项目(60901078;61003079);高等学校博士学科点专项科研基金资助项目(新教师类)(20100203120012)
针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间...
关键词：模型检测 扩展Tempura语言 区间时序逻辑 区间模型 程序规范 统一框架 
支持Stutter-不变性的命题区间时序逻辑
《西安电子科技大学学报》2011年第2期151-156,共6页杨琛 段振华 
国家自然科学基金重大国际合作项目资助项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展计划(973)资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项基金资助项目(JY10000903004)
为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,...
关键词：模型检测 时序逻辑 状态爆炸 
简讯
《西安电子科技大学学报》2011年第1期53-53,共1页
英国德蒙特福德大学计算机科学技术学院软件技术实验室高级研究员B．C．Moszkowski教授日前来校讲学访问．来访期间，B．C．Moszkowski教授分别作了题为“用时间倒序转换时序逻辑”、“使用itl和tempura进行组合推理”、“无穷模型下的...
关键词：区间时序逻辑 计算机科学技术 软件技术 组合推理 公理系统 逻辑分析 专题讲座 分层方法 
基于属性RBAC及委托性质的使用控制模型被引量：2
《汕头大学学报（自然科学版）》2010年第4期57-65,共9页蔡伟鸿 蔡建坤 徐涛 韦岗 
国家自然科学基金-国家杰出青年科学基金项目(60625101);广东省部产学研合作引导项目(2009B090300345);广东省现代信息服务业发展专项(GDIID2008IS046)
针对UCON未涉及特权委托的基本特征和权限管理的缺陷,提出了基于属性RBAC的带委托性质的使用控制模型(EUCON).将角色、委托和扩展属性等要素引入到EUCON,构建了基于属性-角色的访问控制方法,提高了模型的可变性和动态性,并使用区间时序...
关键词：EUCON UCON RBAC 委托 区间时序逻辑 网上行政审批 
基于PVS的ITL定理证明方法被引量：1
《郑州大学学报（理学版）》2009年第4期31-34,44,共5页朱维军 王迤冉 周清雷 
国家863高技术研究发展项目;编号2007AA010408;河南省重大科技攻关项目;编号092101210104;河南省教育厅自然科学研究项目;编号2006520015;2008A520024
介绍了区间时序逻辑ITL的语法、语义和公理系统以及通用的辅助定理证明工具PVS,研究了嵌入ITL到PVS的原理,给出了描述ITL的PVS模块,并给出一个实例,实现了基于PVS的ITL推理.在此基础上可以进一步实现基于PVS的多种扩展ITL推理.
关键词：区间时序逻辑 原型验证系统 辅助定理证明 
区间时序逻辑的模型检查被引量：2
《西安电子科技大学学报》2009年第2期338-342,共5页张海宾 段振华 
国家自然科学基金资助(60873018;60871097);国家自然科学基金重大项目资助(60433010);博士点基金资助(200807010012)
为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规...
关键词：模型检查 时序逻辑 自动机 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部