符号模型检测

作品数：22被引量：40H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：段振华逄涛李祥吴立军苏开乐更多>>
相关机构：西安电子科技大学中山大学贵州大学华东师范大学更多>>
相关期刊：《模糊系统与数学》《软件工程与应用》《计算机应用》《海军工程大学学报》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划贵州省自然科学基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于广义可能性的模态μ演算符号模型检测
《模糊系统与数学》2023年第4期55-64,共10页陈娜 耿生玲 
国家自然科学基金资助项目(12071271,11671244);国家重点研发计划项目(2020YFC1523305);青海省科技援青合作专项(2022-QY-203)
随着计算机功能的不断增强,软硬件系统也变得越来越复杂,使得人们对系统的需求更高。系统建模中可能存在的诸多不确定性信息也亟待被解决,为了充分解决系统信息来源的种种不确定性特征和各种不完备性,本文引入了广义可能性决策过程理论...
关键词：广义可能性决策过程 符号模型检测 有序二值决策图 模态μ演算 
基于不可满足核的近似逼近可达性分析
《软件学报》2023年第8期3467-3484,共18页于忠祺 张小禹 李建文 
国家自然科学基金(62002118,U21B2015);上海市浦江人才计划(19511103602);上海市可信工业互联网软件协同创新中心(2021-2025)。
近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.研究并提出了一种新的模型检测技术,可以有效地对...
关键词：符号模型检测 形式化验证 不可满足核 SAT求解器 不变式 
模糊计算树逻辑的符号模型检测被引量：1
《计算机应用研究》2021年第8期2381-2385,共5页聂朋展 姜久雷 马占有 
国家自然科学基金资助项目(61762002,61962001);宁夏自然科学基金资助项目(2018AAC03127);北方民族大学研究生创新项目(YCX20068)。
对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题。将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储。对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出...
关键词：模糊计算树逻辑 不动点算法 多终端二叉决策图 符号模型检测 
基于符号模型检测的Web服务组合形式化验证被引量：1
《计算机与数字工程》2021年第3期496-501,520,共7页张世杰 徐鹏 刘沛瑶 
国家自然科学基金项目“基于矛盾体分离的动态自动演绎推理研究”(编号:61673320);四川省教育厅项目(编号:18ZB0589)资助。
随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求。Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题。针...
关键词：WEB服务组合 符号模型检测 有限状态自动机 形式化定义 NUSMV 
可能性测度下的CTL符号化模型检测被引量：4
《计算机工程与科学》2018年第11期2008-2014,共7页雷丽晖 郭越 张延波 
国家自然科学基金(A011404)
随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和...
关键词：符号模型检测 可能性测度 CTL 多终端二值决策图 
迁移关系的布尔函数表示的优化
《软件工程与应用》2016年第6期319-326,共8页张小珍 江建国 
符号模型检测中,将迁移关系表示为OBDD的一种较为高效的方法是先借助SMV语言将迁移关系表示为布尔函数,再利用相关算法综合得其OBDD。但在将迁移关系表示为布尔函数时常会遇到两个问题:第一,下一状态取值不确定;第二,具有一定变化规律...
关键词：符号模型检测 OBDD 迁移关系 布尔函数 等效输入变量 
一个命题投影时序逻辑符号模型检测器被引量：3
《软件学报》2015年第8期1968-1982,共15页逄涛 段振华 刘晓芳 
国家自然科学基金(61133001,61202038,61272117,61272118,61322202);国家重点基础研究发展计划(973)(2010CB328102)
现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection tempora...
关键词：符号模型检测 时序逻辑 模型检测器 嵌入式系统验证 
WISHBONE片上总线符号模型检测被引量：1
《计算机研究与发展》2014年第12期2759-2771,共13页逄涛 段振华 
国家"九七三"重点基础研究发展计划基金项目(2010CB328102);国家自然科学基金项目(61003078;61272117;61133001;61272118;91218301;61322202;61202038)
随着多核体系结构的出现和普及,片上总线逐渐成为影响片上系统功能和性能的关键部件.因此,片上总线的验证成为片上系统设计中一个重要组成部分.模型检测作为一种主流的形式化验证方法,可以自动化穷举搜索系统行为以决定片上系统的设计...
关键词：时序逻辑 符号模型检测 WISHBONE总线 片上系统 形式化验证 
Verilog程序的命题投影时序逻辑符号模型检测被引量：5
《西安电子科技大学学报》2014年第2期79-84,共6页逄涛 段振华 刘晓芳 
国家重点基础研究发展计划(973)资助项目(2010CB328102);国家自然科学基金资助项目(61133001)
为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法.依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程...
关键词：时序逻辑 符号模型检测 硬件描述语言 片上系统验证 
基于符号模型检测的SDG模型可诊断性验证被引量：2
《系统工程与电子技术》2011年第2期390-394,共5页宁宁 张骏 高向阳 薛静 
由于定量信息和非线性因果关系的丢失,符号有向图(signed directed graph,SDG)模型的可诊断性需要进一步地进行校核与验证。为此,提出了基于符号模型检测的SDG模型可诊断性形式化验证方法。首先定义了SDG模型的有限状态变迁系统形式化描...
关键词：有向图形学 可诊断性 符号模型检测 符号有向图模型 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部