线性时态逻辑

作品数：33被引量：79H指数：6
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：黄滟鸿钱俊彦赵岭忠周从华蒋屹新更多>>
相关机构：华东师范大学桂林电子科技大学上海丰蕾信息科技有限公司北京航空航天大学更多>>
相关期刊：《微电子学与计算机》《桂林电子科技大学学报》《系统仿真学报》《计算机工程与设计》更多>>
相关基金：国家自然科学基金广西壮族自治区自然科学基金河南省科技攻关计划国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向模型检测的LTL语句自动生成方法被引量：2
《计算机工程与设计》2023年第8期2337-2344,共8页段喜龙 陆智伟 郑巍 陈晋升 樊鑫 肖鹏 
国家自然科学基金项目(61867004)。
为优化线性时态逻辑语句的生成过程,减少模型检测的时间,提出一种面向模型检测的基于自然语言处理生成线性时态逻辑验证语句的方法。对需求文档提取关键词,将文档中的数据和可以代表模型中状态的名词进行提取,注释UML模型,对UML模型中...
关键词：自然语言处理 模型一致性 线性时态逻辑 UML模型 形式化验证工具 模型验证 模型注释 
线性时间属性中近似安全性和活性的刻画
《桂林电子科技大学学报》2022年第5期423-430,共8页常玉婷 潘海玉 
国家自然科学基金(62162014);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(kx201911)。
针对线性时间属性中最重要的基础属性安全性和活性,将它们扩展到模糊背景下,有助于定量刻画系统与其属性之间的满足程度。结合度量理论中线性距离的概念,刻画系统与属性之间关系,进而量化一个系统多大程度满足一个属性。首先回顾线性距...
关键词：线性时间属性 模糊逻辑 安全性 活性 线性时态逻辑 
基于度量线性时态逻辑的近似安全性被引量：2
《计算机科学》2020年第10期309-314,共6页蔡泳 钱俊彦 潘海玉 
国家自然科学基金(61672023);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(kx201911)。
近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基...
关键词：安全性 模型检测 线性时间属性 线性时态逻辑 伪超度量空间 
基于在线模型检验技术的微内核验证
《微纳电子与智能制造》2020年第1期102-109,共8页董星河 郭建 
自然科学基金委重点项目(61532019);上海市重点项目(19511103602)资助。
物联网的兴起,对操作系统的可靠性提出了更高的要求。为确保微内核操作系统的安全性,提出了一种基于事件总线的微内核在线模型验证框架,主要思想是通过映射函数将源代码转换成抽象模型,并从微内核规范中抽取性质。根据源代码的控制流程...
关键词：操作系统 有界模型检查 映射函数 线性时态逻辑 
基于线性时态逻辑的物联网操作系统安全性设计被引量：3
《电子技术应用》2020年第2期92-97,102,共7页张华强 李凯航 王继刚 
根据物联网操作系统安全性设计的需求,同时结合在经典线性时态逻辑、逻辑程序设计、形式化模型检测理论方面的研究与工程实践探索,提出了一种应用于物联网操作系统安全性设计的方法论,并进行了工程原型验证。实践证明该方法的效果符合预...
关键词：物联网操作系统 经典现行时态逻辑 形式化模型检测理论 安全性设计 
基于Büchi自动机化简的JavaMOP监控器构造方法被引量：1
《桂林电子科技大学学报》2019年第5期374-378,共5页叶玲玲 钱俊彦 查显伟 
国家自然科学基金(61562015);广西自然科学基金(2018GXNSFDA138003);桂林电子科技大学研究生教育创新计划(2017YJCX51)
为了提高JavaMOP对程序运行时验证的效率,提出一种基于Büchi自动机化简的JavaMOP监控器构造方法,降低JavaMOP运行时验证的时间和内存开销。该方法将线性时态逻辑(linear temporal logic,简称LTL)描述的属性规范转化为Büchi自动机,利...
关键词：运行时验证 JavaMOP 监控器 线性时态逻辑 BÜCHI自动机 
基于ASP及稳定失败语义的CSP模型检测
《桂林电子科技大学学报》2015年第5期401-407,共7页左贵征 赵岭忠 
国家自然科学基金(61262008;61100186);广西可信软件重点实验室基金(KX201113)
针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实...
关键词：通信顺序进程 线性时态逻辑 稳定失败语义 回答集程序设计 
基于关键迹和ASP的CSP模型检测被引量：3
《软件学报》2015年第10期2521-2544,共24页赵岭忠 翟仲毅 钱俊彦 郭云川 
国家自然科学基金(61262008;61100186);广西自然科学基金(2013GXNSFBA019267);武汉大学软件工程国家重点实验室开放基金(SKLSE20100806);广西教育厅重点项目;广西高等学校高水平创新团队及卓越学者计划;广西可信软件重点实验室基金(kx201113;kx201415);桂林电子科技大学创新团队资助项目
模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有...
关键词：模型检测 通信顺序进程 关键迹模型 线性时态逻辑 回答集程序设计 
基于惰性切片的线性时态逻辑性质验证被引量：1
《吉林大学学报（工学版）》2015年第1期245-251,共7页黄宏涛 王静 叶海智 黄少滨 
国家科技支撑计划项目(2012BAH08B02);河南省科技攻关计划项目(082400420250;112300410008);河南省教育厅科学技术研究重点项目(13A520508);河南师范大学博士科研启动基金项目(qd12107);河南师范大学青年科学基金项目(2013qk33)
惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定Büchi自动机与系统模型...
关键词：计算机软件 模型检测 惰性切片 线性时态逻辑 BÜCHI自动机 乘积自动机 
组合服务安全性检查方法研究
《统计与决策》2013年第23期65-67,共3页顾小林 卞艺杰 浦徐进 曹文彬 蒋勋 
国家自然科学基金资助项目(70901034);教育部人文社科研究规划基金(12YJA630007);中央高校基本科研业务费专项资金资助项目(JUSRP21101);江南大学校人文社科预研项目(2010wyy005);江南大学江苏省食品安全研究基地项目(10SPJD006);江南大学自主科研计划学科交叉创新团队基金(JUSRP31107)
文章针对组合服务安全性检查方法未对服务进行分类处理的问题,将服务分为基本服务和扩展服务,基本服务采用进程元语言建模,借助线性时态逻辑表示基本服务的常规安全标准,通过SPIN模型检查基本服务符合常规安全标准的情况;扩展服务在开...
关键词：线性时态逻辑 进程元语言 简单服务组合语言 物联网 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部