线性时态逻辑中的特性模式 被引量：9

1

作者 黎升洪 缪淮扣 张新林 《计算机应用》 CSCD 北大核心 2006年第8期1912-1915,共4页

在模型检查应用中,需要使用线性时态逻辑对软件具备的特性进行描述。虽然,不同应用背景涉及不同方面的特性描述,但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性,首先,按照线性时态逻辑所描述性质划分,常见性... 在模型检查应用中,需要使用线性时态逻辑对软件具备的特性进行描述。虽然,不同应用背景涉及不同方面的特性描述,但是线性时态逻辑描述软件特性方式上具有共性。本文从两个方面抽取这种共性,首先,按照线性时态逻辑所描述性质划分,常见性质包括活性、安全性等;其次,按照线性时态逻辑公式的作用范围划分。通过对共同问题,找到共同的描述方法得到线性时态逻辑的特性模式。最后介绍了线性时态逻辑特性模式在SPIN中的应用。 展开更多

关键词 线性时态逻辑 特性模式 模型检查 SPIN

下载PDF 职称材料

基于线性规划的RTL可满足性求解和性质检验 被引量：7

2

作者 郑伟伟 吴为民 边计年 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2006年第4期538-544,共7页

采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题·深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法·通过将RTL性质转化为虚拟RTL电路,找到了... 采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题·深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法·通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法·通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势· 展开更多

关键词 线性规划 寄存器传输级 可满足性 性质检验 形式验证

下载PDF 职称材料

基于关系演算的Java模式识别 被引量：5

3

作者 苗康 余啸 +1 位作者 赵吉 沈宇 《计算机应用研究》 CSCD 北大核心 2010年第9期3425-3430,共6页

分析了面向对象类与对象间的关系,在此基础上建立了对应的属性模型并且以关系演算的方法进行捕获模型的对象关系;讨论并实现了动、静态相结合的基于Java语言的经典设计模式检查工具,并以该工具为基础做实验对一些设计模式进行了验证。

关键词 关系演算 设计模式 JAVA虚拟机 属性检查

下载PDF 职称材料

自适应软件动态过程时间特性建模与验证方法 被引量：4

4

作者 韩德帅 邢建春 +1 位作者 杨启亮 李决龙 《计算机应用》 CSCD 北大核心 2018年第3期799-805,共7页

现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性(监控周期、延迟触... 现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性(监控周期、延迟触发时间、自适应过程截止时间、自适应调节时间和稳定时间等);然后,构造了一种基于时间自动机网络(TAN)的自适应软件动态过程时间特性建模模板;最后,将自适应软件时间特性描述为定时计算树逻辑(TCTL)的形式,并对时间特性进行了形式化分析和验证。结合具体案例验证了该自适应软件时间特性建模和验证方法,结果表明该方法能够显式刻画自适应软件时间特性,降低其形式化建模的难度。 展开更多

关键词 自适应软件 时间特性 形式化方法 时间自动机 模型检验

下载PDF 职称材料

青海同仁市自然资源资产清查核算处理方法研究

5

作者 李玉梅 《矿产与地质》 2024年第3期602-608,共7页

在对同仁市自然资源资产清查过程中,采用准备工作→数据收集→价值估算→成果汇总→检查验收的清查方法流程。针对清查过程中出现的耗费时间长、部分实物量清查信息缺失、部分数据缺失或不完善等问题,在利用现有资料和实地调查的基础上... 在对同仁市自然资源资产清查过程中,采用准备工作→数据收集→价值估算→成果汇总→检查验收的清查方法流程。针对清查过程中出现的耗费时间长、部分实物量清查信息缺失、部分数据缺失或不完善等问题,在利用现有资料和实地调查的基础上,创新性提出了针对同仁市清查所采用的宗地图斑编号、不动产数据偏差处理、无矿区范围的处理、矿区范围重叠的处理、空洞无属性图斑处理等技术。通过对同仁市全民所有土地、矿产、森林、草原、湿地等自然资源开展实物量和价值量清查,得到了同仁市自然资源资产情况。结果表明,结合所有自然资源资产清查工作实践,完成各门类自然资源资产数据清查工作的冗余图斑、数据空间信息要素层空洞区域的处理,在一定程度上提升工作成效。研究成果可为自然资源资产清查核算提供参考。 展开更多

关键词 资产清查 自然资源 土地资源 青海同仁市

下载PDF 职称材料

数据和时间感知的Web服务组合模型检测 被引量：2

6

作者 狄浩军 戎玫 +1 位作者 张广泉 朱稷涵 《计算机科学》 CSCD 北大核心 2011年第11期123-126,136,共5页

为了验证Web服务组合中的数据属性和时间属性,提出了一种基于数据和时间感知的服务模型DTSM的Web服务组合模型检测方法。首先将BPEL描述的Web服务组合转换为含有数据流信息和时间信息的形式化模型,然后将该模型映射至UPPAAL规约,最后应... 为了验证Web服务组合中的数据属性和时间属性,提出了一种基于数据和时间感知的服务模型DTSM的Web服务组合模型检测方法。首先将BPEL描述的Web服务组合转换为含有数据流信息和时间信息的形式化模型,然后将该模型映射至UPPAAL规约,最后应用模型检测工具UPPAAL实现了Web服务组合的正确性验证。 展开更多

关键词 WEB服务组合 数据属性 时间属性 BPEL 模型检测

下载PDF 职称材料

计算树逻辑特性模式研究 被引量：3

7

作者 周慧 《计算机工程》 CAS CSCD 北大核心 2009年第23期68-70,共3页

模型检查是系统验证的有效方法,在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画,然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义,根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式,包括缺... 模型检查是系统验证的有效方法,在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画,然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义,根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式,包括缺失性模式、存在性模式、普遍性模式、优先性模式和跟随性模式等。 展开更多

关键词 计算树逻辑 特性模式 模型检查

下载PDF 职称材料

带时间约束的LTL性质的模型检测的实现 被引量：2

8

作者 部德振 《计算机工程与设计》 CSCD 北大核心 2011年第2期564-567,共4页

针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束... 针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。 展开更多

关键词 时间自动机 模型检测 线性时序逻辑性质 时间约束 空性检测

下载PDF 职称材料

基于度量线性时态逻辑的近似安全性 被引量：2

9

作者 蔡泳 钱俊彦 潘海玉 《计算机科学》 CSCD 北大核心 2020年第10期309-314,共6页

近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基... 近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基础属性,能保证系统在运行过程中不会发生“坏”的事情,其在度量背景下的推广形式也应该得到关注。为此,文中研究伪超度量空间上安全性的扩展问题,首先对已有的度量线性时态逻辑进行适当的补充,使其能充分地刻画度量背景下的线性时间属性;然后引入距离阈值α,提出一种α-安全性的概念,从而将经典的安全性提升到伪超度量空间上;最后讨论度量线性时态逻辑与α-安全性之间的关系。这些结论为取值于度量空间的系统的安全性验证提供了理论依据。 展开更多

关键词 安全性 模型检测 线性时间属性 线性时态逻辑 伪超度量空间

下载PDF 职称材料

基于CATIA/CAA数模属性自动校验技术研究 被引量：1

10

作者 韩志仁 陈帅 《沈阳航空航天大学学报》 2011年第1期1-4,共4页

针对在CATIA中使用人工审核方法检测工装数模规范性时效率低、易漏检等问题,提出了一种对工装数模规范性进行自动校验的方法。该方法基于CAA,以CATIA为平台,Visual C++为编程工具,能够自动快速准确进行检验,解决了订货单信息、数模信息... 针对在CATIA中使用人工审核方法检测工装数模规范性时效率低、易漏检等问题,提出了一种对工装数模规范性进行自动校验的方法。该方法基于CAA,以CATIA为平台,Visual C++为编程工具,能够自动快速准确进行检验,解决了订货单信息、数模信息自动获取的难题。缩短了工装设计周期中用于校验的时间,提高了工作效率,为模具设计部门对工装数模规范性实现高效检测提供了帮助。 展开更多

关键词 数模 属性 自动校验 CATIA CAA

下载PDF 职称材料

浅谈企业财产清查工作 被引量：1

11

作者 闫永红 魏明惠 《洛阳工业高等专科学校学报》 2004年第2期60-61,共2页

结合国内、国际内审理论研究、发展方向,以及多年来内审工作实践,提出内部审计企事业单位内部的一种经济监督活动,是以服务者的身份出现在企事业单位经济活动的各个环节,并为单位领导提出各种建没性建议的审计,而不是国家政府审计职能... 结合国内、国际内审理论研究、发展方向,以及多年来内审工作实践,提出内部审计企事业单位内部的一种经济监督活动,是以服务者的身份出现在企事业单位经济活动的各个环节,并为单位领导提出各种建没性建议的审计,而不是国家政府审计职能的延伸。 展开更多

关键词 财产清查 国有资产 安全完整

下载PDF 职称材料

用模型检验产生安全性质的测试 被引量：1

12

作者 曾红卫 缪淮扣 《应用科学学报》 EI CAS CSCD 北大核心 2011年第5期529-536,共8页

安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,... 安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,"先验证再测试"的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例.给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法.使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例. 展开更多

关键词 安全性质 模型检验 测试生成 危险迹

下载PDF 职称材料

斜坡桥基力学性能控制指标回归分析研究 被引量：1

13

作者 邹静蓉 《公路工程》 2008年第6期16-19,共4页

利用数理统计理论,通过对影响斜坡桥基承载力的各因素,包括桩径、桩长、桩身材料、岩体特性、桥基位置及斜坡坡度等进行回归分析,拟合出求解斜坡桥基承载力的一般表达式,对斜坡桥基的设计具有一定的指导意义。

关键词 斜坡桥基 力学性能 数理统计 回归分析 模型检验

下载PDF 职称材料

基于CDFG和OVL的系统验证性质分类 被引量：1

14

作者 朱明 边计年 吴为民 《计算机工程》 EI CAS CSCD 北大核心 2005年第10期48-50,共3页

在数据控制流图(CDFG)结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力。通过对OVL语言和CTL描述进行改进,针对模拟验证、CDFG图匹配、模型检测3种方法设计相应的性质,实... 在数据控制流图(CDFG)结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力。通过对OVL语言和CTL描述进行改进,针对模拟验证、CDFG图匹配、模型检测3种方法设计相应的性质,实验结果表明这种分治验证策略有助于提高系统验证的效率和规模。 展开更多

关键词 模拟 形式验证 性质 模型检测 数据控制流图

下载PDF 职称材料

非经典切片技术及其在形式验证中的应用综述

15

作者 高新岩 吴尽昭 +1 位作者 闫炜 周宁 《计算机工程与应用》 CSCD 北大核心 2007年第36期43-47,54,共6页

切片技术最初是作为一种程序分解抽取的分析技术而出现的,经过20多年的不断发展和完善,应用范围已遍及软件工程学科的各个方面。特别是从本世纪初,随着非经典切片:计算切片和证明切片两个新兴研究方向的出现,其学术研究和工程价值越发... 切片技术最初是作为一种程序分解抽取的分析技术而出现的,经过20多年的不断发展和完善,应用范围已遍及软件工程学科的各个方面。特别是从本世纪初,随着非经典切片:计算切片和证明切片两个新兴研究方向的出现,其学术研究和工程价值越发突出。简要地介绍了切片技术思想的起源、发展过程,并着重介绍非经典的计算切片和证明切片技术及其在验证领域的应用。 展开更多

关键词 程序切片 计算切片 证明切片 约简 形式验证 性质验证 模型检验

下载PDF 职称材料

一种基于SystemC属性检查的验证方法

16

作者 王胜 赵瑞莲 《现代电子技术》 2009年第8期52-55,59,共5页

当今复杂电子系统倾向于在更高抽象级进行建模,一种基于C/C++的硬件描述语言,SystemC语言变得非常重要。在此探讨了一种基于SystemC属性检查的仿真验证方法。针对电路系统的线性时态逻辑属性,定义了属性表达的基本形式,并用SystemC代码... 当今复杂电子系统倾向于在更高抽象级进行建模,一种基于C/C++的硬件描述语言,SystemC语言变得非常重要。在此探讨了一种基于SystemC属性检查的仿真验证方法。针对电路系统的线性时态逻辑属性,定义了属性表达的基本形式,并用SystemC代码描述系统属性,在仿真中检查系统属性从而达到验证目的。首先介绍SystemC语言及一种基于SystemC的属性检查方法,讨论了现有方法的不足之处,并给出了两种改进方案,最后通过实验证实该方案的有效性,同时实验表明该改进方案在仿真性能上有很大的提高。 展开更多

关键词 SYSTEMC 属性检查 属性链 复杂电子系统

下载PDF 职称材料

基于分离逻辑的并行程序性质验证方法

17

作者 万良 石文昌 冯慧 《计算机科学》 CSCD 北大核心 2013年第10期148-154,共7页

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出。并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大。为此,提出一种基于分离逻辑的新的验证方... 随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出。并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大。为此,提出一种基于分离逻辑的新的验证方法。该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值。实例进一步说明,此方法更有效,同时也简化了验证的规模。 展开更多

关键词 霍尔逻辑 分离逻辑 并行程序 逻辑组合式 性质验证

下载PDF 职称材料

认证协议相关性分析

18

作者 张亚英 梁坚 尤晋元 《通信学报》 EI CSCD 北大核心 2002年第1期103-110,共8页

本文提出认证协议的相关性问题,并引入关联因子的概念,从消息相关和协议相关两个层次上对相关性进行描述,同时将协议的运行看作是攻击者和协议环境交互的模型。我们用CSP的模型检查工具FDR2对该模型进行形式化描述,以著名的Needham-Schr... 本文提出认证协议的相关性问题,并引入关联因子的概念,从消息相关和协议相关两个层次上对相关性进行描述,同时将协议的运行看作是攻击者和协议环境交互的模型。我们用CSP的模型检查工具FDR2对该模型进行形式化描述,以著名的Needham-Schroeder 公钥协议为例分析其相关性,得出了理想的结果。 展开更多

关键词 认证协议 关联因子 通信协议

下载PDF 职称材料

电路并发性质在GSTE中的研究和实现

19

作者 郑德生 杨国武 徐忠林 《微电子学与计算机》 CSCD 北大核心 2013年第6期43-47,共5页

由于GSTE的性质描述断言图的时序特性,使其不能够简洁易懂地描述电路的并发性质,因此将meet运算符引入GSTE,重新定义GSTE断言图及其验证算法,使之能更简洁的描述和验证数字电路的并发性质,实验表明引入meet运算符后的算法能够降低验证... 由于GSTE的性质描述断言图的时序特性,使其不能够简洁易懂地描述电路的并发性质,因此将meet运算符引入GSTE,重新定义GSTE断言图及其验证算法,使之能更简洁的描述和验证数字电路的并发性质,实验表明引入meet运算符后的算法能够降低验证的复杂度. 展开更多

关键词 GSTE形式化验证 并发性质 模型检验 断言图

下载PDF 职称材料

基于类型理论的安全协议验证技术

20

作者 宋震 李舟军 窦文华 《计算机工程与科学》 CSCD 2005年第3期7-9,25,共4页

基于类型理论的安全协议验证技术是近年来新出现的技术途径之一。本文在对基于类型理论的安全协议验证技术及其研究现状进行简要介绍后,主要分析了由A. D. Gordon建立的、用于对协议的认证性进行验证的类型系统,借助其与信念逻辑方法在... 基于类型理论的安全协议验证技术是近年来新出现的技术途径之一。本文在对基于类型理论的安全协议验证技术及其研究现状进行简要介绍后,主要分析了由A. D. Gordon建立的、用于对协议的认证性进行验证的类型系统,借助其与信念逻辑方法在证明过程中的某些相似性,对其中的主要思想进行了分析讨论。本文最后还指出了基于类型理论的安全协议验证技术研究中一些有待深入的问题。 展开更多

关键词 计算机网络 网络安全 类型理论 安全协议验证技术 信念逻辑

下载PDF 职称材料