线性时序逻辑

作品数：73被引量：185H指数：8
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：欧林林禹鑫燚郭永奎李永明肖云涛更多>>
相关机构：浙江工业大学国防科学技术大学中国科学院软件研究所清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划浙江省自然科学基金国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机科学x
共 条 记 录，以下是1-6
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于活性顺序图的运行时验证研究被引量：1
《计算机科学》2016年第8期137-141,164,共6页叶俊民 张坤 叶竹君 陈盼 陈曙 
国家科技支撑计划项目(2015BAK33B00);中央高校基本科研业务费专项资金科研项目(CCNU15GF003);教育部人文社会科学研究规划基金(15YJA880095)资助
运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重...
关键词：活性顺序图 线性时序逻辑 重写逻辑 运行时验证 
一种结合线性时序逻辑和故障树的软件安全验证方法被引量：3
《计算机科学》2015年第12期71-75,共5页王飞 沈国华 黄志球 马琳 刘畅 李海峰 廖莉莉 
国家自然科学基金(61272083);国家高技术研究发展计划(863)(2009AA010307);国家国防科技工业局技术基础科研项目(Z052013B009;JSJC2013205C507)资助
嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线...
关键词：故障树分析 模型检验 线性时序逻辑 安全关键系统 安全属性 
多处理器任务调度算法TDS的建模与验证被引量：5
《计算机科学》2012年第11期301-304,F0003,共5页李召妮 雷丽晖 李永明 
国家自然科学基金(60873119;61003061);高校博士学科点专项科研基金(20090202120006);中央高校基本科研业务费(GK200902017;GK201001003)资助
在多处理器系统中,一个应用所要完成的任务可以分配给同一个处理器处理,也可以分配给多个处理器处理,所以传统的测试方法难以满足多处理器任务调度算法的验证。在此,提出一个基于扩展Büchi自动机的形式化模型,并用该模型来描述多处理...
关键词：多处理器调度算法 线性时序逻辑 模型检测 扩展Büchi自动机 
基于K-模拟的抽象
《计算机科学》2007年第9期242-244,共3页袁志斌 徐正权 王能超 
国家自然科学基金(70271069)的支持
尽管近年来模型检测取得了很大的进步,但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中,抽象技术是最有效的方法之一。本文给出了基于K-模拟的抽象的高效算法,并证明了在线性时序逻辑框架下抽象的可靠性和完备性。
关键词：抽象 线性时序逻辑 K-模拟 
Petri网性质的线性时序逻辑描述与Spin检验被引量：1
《计算机科学》2006年第5期287-289,共3页段风琴 李祥 
贵州省科学基金项目(GGY2004002)
Petri 网是描述并发系统的很直观的图形工具;Spin 是一种著名的分析验证并发系统性质的工具。本文首先论述 Petri 网性质的线性时序逻辑描述,研究用 Promela 编程描述 Petri 网和用 Spin 对 Petri 网性质进行检验的方法,最后通过两个具...
关键词：模型检测 SPIN PROMELA PETRI网 线性时序逻辑 
程序时序属性的自动测试
《计算机科学》2004年第6期132-134,179,共4页马晓东 董威 王戟 齐治昌 
测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中,作者设计并实现了一种根据程序的线性时序逻辑(LTL)的性质产生测试预言的方法。首先,作者将一线性时序逻辑公式转换为一个有限状态自动机,然后,管理源代码,以便抽取与线...
关键词：测试预言 线性时序逻辑 FSA LTL 状态自动机 反应式系统 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部