行为时序逻辑

作品数：22被引量：25H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李均涛李祥唐郑熠万良吴勇更多>>
相关机构：贵州大学贵州财经大学福建工程学院山西大学更多>>
相关期刊：《网络空间安全》《计算机应用研究》《计算机光盘软件与应用》《计算机技术与发展》更多>>
相关基金：国家自然科学基金贵州省自然科学基金中央高校基本科研业务费专项资金美国GENECHIU基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于行为时序逻辑的多方协作取证研究被引量：1
《网络空间安全》2016年第11期82-86,共5页李均涛 唐郑熠 张金磊 
论文提出了一种基于行为时序逻辑和片面性理论的多方协作取证的形式化方法,有望在多方参与的调查取证中验证不可观察的行为证据,并将其应用到一个取证实例中。
关键词：入侵取证 行为时序逻辑 片面性 多方协作取证 
行为时序逻辑中四级公平性下的活性推理规则
《计算机应用研究》2016年第10期3045-3048,共4页唐郑熠 薛醒思 王金水 王晓峰 
福建省自然科学基金计划资助项目(2016J05146);国家自然科学基金资助项目(61503082);福州市科技基金资助项目(2012-G-126);福建工程学院科研启动基金资助项目(GY-Z13112)
公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,...
关键词：行为时序逻辑 公平性 活性 推理规则 系统验证 
一种基于TLA的解决N皇后问题的方法
《贵州大学学报（自然科学版）》2016年第1期86-88,共3页台亚非 龙士工 
国家自然科学基金项目资助(61163001)
行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5...
关键词：行为时序逻辑 模型检测 N皇后问题 TOOLBOX 
互斥协议的安全性分析
《计算机应用研究》2015年第5期1486-1488,共3页赵梦龙 唐郑熠 万良 韦立 
国家自然科学基金资助项目(6130900);贵州省自然科学基金资助项目(J[2011]2328);福建工程学院科研启动基金资助项目(GY-Z13112)
安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转...
关键词：互斥协议 属性分类 安全性 活性 行为时序逻辑 
基于行为时序逻辑系统性质研究
《信息安全与技术》2014年第12期17-19,共3页李均涛 
贵州省自然科学技术基金(黔科合J字[2012]2096号);贵州财经大学人才引进科研基金
文章研究行为时序逻辑(TLA)中行为(Action)的性质及行为之间的关系,提出"行为活性"和"行为安全性"概念,从行为的视角重新给出系统活性和安全性的定义,使得安全性和活性定义更加直观和容易理解,并证明了新老定义的等价性。
关键词：行为时序逻辑 活性 安全性 安全行为 
一种安全转移系统模型的构造及其运用
《计算机应用研究》2014年第2期558-562,共5页万良 肖源 
国家自然科学基金资助项目(61163001);中国人民大学科学研究基金(中央高校基本科研业务费专项资金资助)项目成果(+12 XNLF06);贵州自然科学基金项目(J[2011]2328)
为提高安全性,一般利用密码技术,但系统运行过程的安全尚显不足,为此基于行为时序逻辑TLA提出一种安全转移系统模型。通过设置安全属性,构造安全行为,使得系统在运行过程中的每次转移都满足安全属性,从而提高过程的安全性。为此,定义初...
关键词：形式化方法 行为时序逻辑 安全性 安全行为 安全转移系统 
行为时序逻辑与自反线性时序逻辑的关系
《现代计算机（中旬刊）》2014年第1期3-7,共5页白金山 冯天亮 吴应江 丘文峰 王梦 
广东医学院博士启动基金(No.B2011006)
为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中,对行为时序逻辑公式的语义进行形式化定义,从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系,提出并证明行为时序逻辑公式转换...
关键词：模型检测 行为时序逻辑 语义 语法 自反性 
基于行为时序逻辑的磁盘入侵取证研究
《电脑知识与技术（过刊）》2013年第9X期5820-5821,5832,共3页李均涛 
贵州省自然科学技术基金(黔科合J字[2012]2096号);贵州财经大学人才引进科研基金
运用假设行为时序逻辑理论体系对磁盘的文件系统进行描述,建立入侵系统模型,使用模型检测工具予以取证。该方法的目标是在反侦察攻击环境下,即在证据缺失的情况下,也能顺利地进行取证调查。
关键词：入侵取证 行为时序逻辑 模型检测 磁盘技术 
基于行为时序逻辑TLA的算法分析与验证
《计算机光盘软件与应用》2013年第18期74-75,共2页赵梦龙 
行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑,它结合了行为逻辑和时序逻辑的特点,增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了D...
关键词：行为时序逻辑 PlusCal TOOLBOX DEKKER算法 
并发系统中谓词行为图的行为时序逻辑表达
《计算机应用研究》2013年第9期2752-2754,共3页黄贻望 袁科 
中央高校基本科研业务费专项资金资助项目(2012211020201);贵州省科学技术厅;铜仁市科学技术局;铜仁学院联合基金资助项目(黔科合J字LKT[2012]04号;黔科合J字LKT[2012]24号);铜仁学院科研启动基金资助项目(TS10013)
行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图,对于并发转移可以用...
关键词：并发性 规约 谓词行为图 行为时序逻辑 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部