基于UML的建模及模型检验研究

UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UUL模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建模的基础上把UML模型转换为SMV模型,然后使用符号模型检验器（SMV）对模型进行检验,有利于在系统的设计早期发现系统的缺陷。     

基于符号模型检验的硬件验证

随着程序或电路规模的增大，状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面，可以处理大规模的数据和控制序列，缓和了组合爆炸的问题。文章介绍了符号模型检验的原理和方法，利用验证工具VIS验证了8位微处理器PIC的一些关键属性，并给出实验结果。     

面向模型检验的UML状态机语义

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图．它丰富的表示符号提供了强大的描述机制，但也降低了其结构的模块性，提高了对其分析验证的难度．模型检验是自动检验有限状态并发系统的技术．通过模型检验SM描述的不同系统元素的行为是否满足某些性质，能尽早发现设计中的错误．为了将模型检验技术应用于SM的验证，本文用kripke结构定义SM的操作语义．与已有的SM语义定义不同，本文考虑到了SM中包含的不确定因素，用kripke结构描述系统所有可能的演化轨迹、通过检验从SM翻译得到的kripke结构达到模型检验SM的目的．     

面向模型检验的UML状态机语义

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.     

论CCD相机标定的内、外因素：畸变模型与信噪比

决定ＣＣＤ相机定标的精度不仅取决于成像系统中已存在的各种畸变（模型），同时取决于这些畸变在数据噪声中所占的比例－信噪比，前者称为决定相机标定精度的内在因素，后者称为决定相机标定精度的外在因素。本文提出了利用统计显著性检验、相关系数检验来选择畸变模型。各种不同的模拟数据及实际数据试验表明：（１）不同的成像系统中畸变模型是不一致的，必须用显著性检验方法来检验畸变模型是否显著，删除非显著性畸变；（２）在选择多个畸变参数作为畸变模型时，畸变参数之间、畸变参数与标定参数之间有时存在强相关，必须用相关性检验这些参数，删除强相关畸变参数。本文还提出了用畸变在数据噪声中所占有的比例－信噪比作为衡量以多高的精度去量测影像坐标才能补偿畸变的标准，模拟试验数据表明：信噪比越大，畸变越能补偿；反之补偿就小．而且定标精度与信噪比是指数函数关系。     

ARIMA模型的介绍

本文基于时间序列理论,对数据进行平稳化处理、模型定阶、参数估计,建立模型,并对模型进行检验,深刻了解了ARIMA模型,为生活中的实际应用打下基础。     

攻击图的网络威胁自动建模方法研究

为了增强网络的安全性,对网络整体进行威胁分析和评估应用,结合攻击图的特点,研究并提出了一种攻击图的网络威胁自动化建模方法。在攻击图生成之前,抽象出网络威胁数学模型,包括主机信息、拓扑信息、漏洞信息和攻击者信息四个组成部分。并针对所建的网络威胁模型提出自动建模方法和具体的自动化流程。基于此,结合攻击事件的Büchi模型和CTL描述,使用符号模型检验算法自动生成攻击图,为攻击图的应用奠定基础。     

片上系统的模型检验

片上系统(SoC)的验证是一个比较复杂的问题，仅靠模拟仿真无法保证SoC设计的正确。形式化方法是利用数学推理的方法来证明其正确．是对SoC设计进行验证的一条重要途径。模型检验技术是一种完全自动化的形式化方法，针对模型检验技术，讨论了在SoC验证中的应用，指出在SoC设计中，只有把模拟仿真与形式化、半形式化的方法结合起来，才能更好的对SoC进行验证。     

图像序列的运动目标选择技术

本文利用最小二乘法导出了图像局部灰值分布的二元二次多项式系数和最佳估计量，并且把剩余成份看成零均值白噪声，由此建立了二次型模型，它是对局部灰值分布的最好逼近。为了从图像序列中检测帧间变化，基于二次型模型导出了服从Ｆ（ｎ＋３，２ｎ－１２）分布的统计假设检验模型，其中ｎ为检测窗内的象素数目。因为只有Ｆ检验一般还不能够从变化检测中选择出运动目标，本文利用专门设计的聚类分析和补空洞技术，能使目标损失和虚警     

模型检验技术的研究与应用

本文首先介绍模型检验技术的概念,然后详细介绍模型检验技术的组成部分以及利用模型检验技术进行模块验证的流程,并利用总线仲裁的实例进行讲解分析,最后对模型检验技术进行总结和展望.     

浅析模型检测技术

模型检测是一种能够自动验证有限状态并发系统技术.通过显式状态搜索来验证有限状态并发系统的模态与命题性质,当前已被广泛应用于计算机软硬件系统安全性能的检测.本文浅析了模型检测技术,分析了模型检测技术的发展概况、基本原理、算法、模型检测工具等,并介绍了模型检测领域的最新进展.     

模型检测:理论、方法与应用

随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.模型检测的研究大致涵盖以下内容:模态/时序逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制.这几个方面之间有着密切的内在联系.不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往往是针对某些特定类型的逻辑公式.本文将就这几个方面分别加以阐述,最后介绍该领域的新进展.     

基于模型检测的URA—SAP安全性验证

在RBAC访问控制系统的安全性分析问题（RBAC—SAP）中,用户-角色分配相关的安全性分析问题（URA—SAP）是其中最重要的一个子问题,即用户-角色分配关系的变化对系统安全性的影响问题。提出了一种将URA—SAP转化为模型检测问题的自动化验证算法,实验表明采用该算法并结合现有的模型检测工具可以有效地解决URA—SAP问题。     

概率时态认知逻辑模型检测中三值抽象技术的研究

 为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.     

基于Craig插值的线性混成系统符号化模型检测

最强后件的计算是模型检测算法的核心.本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式,利用一阶逻辑公式不可满足情况下的插值存在性定理,对线性混成自动机的有界模型检测公式进行指定的划分,使用支持线性算术插值计算的可满足性模理论后端证明引擎的线性时间复杂度的消解反证技术获得这两部分公式间的插值公式,按一阶逻辑Craig插值的性质,所得到的插值公式就是模型检测过程中最强后件公式的上近似表示.有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式,也不需像有界模型检测按步长展开变迁公式进行可满足性判定.最后本文在此最强后件计算的基础上,以有界模型检测技术作为反例确认方法,实现了一种无假反例的混成系统近似可达集计算算法.实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能.     

基于SPIN的模块化模型检测方法研究

该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。     

可信密码模块的模型检测分析

根据可信密码模块规范的非形式化描述,利用模型检测工具SPIN对可信密码模块安全性进行形式化分析,给出了可信密码模块形式化分析的基本框架,重点分析了AP授权协议和可信密码模块初始化子系统.指出了AP授权协议存在的缺陷,并给出了具体的改进措施;同时验证可信密码模块初始化子系统状态的一致性.     

离散时间区间时序逻辑可满足性的判定

目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.     

缓冲区溢出漏洞精确检测方法研究

 缓冲区溢出漏洞是影响系统安全性的严重问题之一,本文提出了一种利用模型检测技术对代码中潜在的缓冲区溢出漏洞进行精确检测的方法.该方法通过静态分析,先将对缓冲区漏洞的检测转化为对程序某个位置可达性的判定.然后,利用模型检测技术对可达性进行验证.基于GCC和Blast,我们使用这一方法构造了一个精确检测缓冲区溢出漏洞的原型系统.最后,使用该原型系统对wu-ftpd,minicom和CoreHTTP等三个实际应用程序进行了检测,结果不仅检测出了已知的漏洞,而且发现了一些新漏洞.