程序重构预处理在提高软件模型检测效率中的应用

针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明:程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.     

基于扩展有限状态机模型的故障检测

提出了基于扩展有限状态机的故障检测模型和检测算法。该模型对软件中的故障进行了形式化定义和描述,检测算法对故障模型中的状态变迁进行缩减,检测故障模型的部分状态变迁,进而可以有效缓解状态空间过大而引起的时间和空间效率问题,从而最大限度地发现被测系统中的故障;最后给出了一个简单协议来加以分析和验证。实验表明,该算法可以快速准确地定位软件中故障发生的位置。     

收缩候选回溯集的有状态动态偏序归约方法

在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的计算成本过高。为此,形式化定义收缩候选回溯集,消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各交织的回溯点,使用当前收缩候选回溯集更新相应回溯集,实现基于有状态动态偏序归约方法的并发多线程程序验证。实验结果表明,与现有动态偏序归约方法相比,该方法能减少遍历迁移数,加速回溯集更新,提高动态软件模型检测效率。     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

基于Petri网的模型检测研究

模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.     

林业信息系统模型检测应用方法研究

模型检测作为一种形式化验证技术已成功应用于硬件以及协议的性质验证过程,目前正转向软件验证领域并逐渐扩展其应用范围。针对特定的森林防火专家系统的知识库规则,研究其所需满足的性质规范的形式化验证问题。首先将规则体描述为状态迁移图,通过引入转换函数对状态迁移图的变迁过程及状态性质进行了有效说明,然后将性质规范描述为相应的时序逻辑表达式,最后通过实例对模型检测过程进行了详细说明,本文的研究成果有效地说明了将模型检测应用于森林防火专家系统等林业信息系统的可行性与正确性。     

基于时序的离散事件系统的可诊断性

提出一种基于事件之间的时序关系判定可诊断性的方法。首先通过添加通讯事件把全局模型分解成几个局部模型来缩减模型的规模,删除局部模型中的无用路径以降低状态空间;其次利用通讯事件和可观测事件之间的时序关系,对受限局部模型的可诊断性进行判定,得出几个判定性质,然后把这些性质运用到局部模型的可诊断性判定中,以避免同步操作的高复杂性;最后通过实例对可诊断性判定的过程进行分析。     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

程序切片技术在并发程序模型检查中的应用

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。     

基于状态模型的四次握手协议验证

利用外部和内部事件状态模型方法抽象出四次握手协议的逻辑过程，并建立协议中重要性质的形式化模型（例如：消息发送顺序、分配密钥等）。Spin工具的特性是对状态模型和性质进行模型检测，通过对模型进一步检测和验证结果的分析，得出四次握手协议在密钥GTK分配上具有一定缺陷。并会导致GTK传送失败。     

基于UPPAAL的微内核操作系统程序验证方法研究

随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题。形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术。形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类。文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证。     

BDD-based software verification

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable’s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.     

航天嵌入式软件整数溢出的形式化验证方法

整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明：该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.     

软件模型代数性质的程序化验证

软件模型代数的思想是通过引入进程代数来对软件体系结构进行建模。它将构件解释为变量,将连接子抽象为代数运算,并针对软件的特性建立了软件体系结构代数模型。在代数模型的基础上,讨论分析获得一系列能指导软件演化的代数性质。但是,上述研究都只对模型的代数性质进行了理论证明,实际上并无程序能够证明这些代数性质的正确性,同时也未给出这些性质的应用方法,使其缺乏可操作性。采用程序化验证的方法对代数性质进行了验证,并对这些性质的应用算法进行了研究,进一步丰富了软件的建模理论,也使得软件演化从理论研究转化为实际应用成为可能。     

一种自动的形式化验证技术-模型检测

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.     

基于分存策略的软件保护博弈模型

软件保护技术普遍是通过完善代码和应用加密方案来达到保护软件的目的。针对软件代码的静态授权抗攻击能力以及软件加密的加密强度是否足够抵抗攻击的问题,提出一种基于分存策略的软件保护博弈模型。该模型采用分存策略对密钥进行分段,得到多个检验与抵抗软件破解者攻击的验证函数,把它们隐藏在程序中,使得软件运行时有多个不同的验证函数对程序进行保护。从博弈论的角度分析论证该模型,并将其应用于软件注册码验证的实例中,提高了软件代码的安全性。实验结果和分析表明了该模型的正确性和有效性。     

Termination of nondeterministic quantum programs

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space, which formalize the quantum mechanical behaviors of the machine. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes, and at each step of an execution a process is chosen nondeterministically to perform the next action. This execution model formalize the users’ behavior of calling the processes in the classical world. Applying the model to a quantum walk as an instance of physically realizable systems, we describe an execution step by step. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space.     

基于Trnsys的水冷型中央空调系统建模与仿真

以广州某大厦水冷型中央空调系统为例子,利用Trnsys建立了大厦某层的多区域建筑及其中央空调系统能耗仿真模型,在此基础上分析加控制和不加控制2种情况下中央空调能耗情况。由2种模型的仿真结果可知中央空调具有很大的节能空间。模型主要用于研究中央空调运行的一些性质,对中央空调的节能优化控制具有重要的意义。     

基于分段模型检测的云服务跨域认证协议的形式化分析与验证

针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。