基于模型检验的构件验证技术研究进展

模型检验以其自动化程度和完备性高、与构件技术互补性强等特点,在软件构件可信性质的分析和验证中发挥着日益重要的作用.将基于模型检验的构件验证方法分为基于系统规约模型的验证和基于源代码的验证,分别对其研究现状和发展动态进行了详细的综合评述.首先对模型检验与构件可信性质验证的关系进行了探讨,接着对基于SOFA,Fractal,CORBA及各种特定构件模型的验证方法和基于转化思想的源码验证、面向源码的直接验证及面向可执行代码的动态验证方法分别进行了评述.最后,指出了基于模型检验的构件验证技术所面临的主要挑战和未来的发展方向.     

On the Effective Deployment of Functional Formal Verification

We examine IBM's exploitation of formal verification using RuleBase—a formal verification tool developed by the IBM Haifa Research Laboratory. The goal of the paper is methodological. We identify an integrated methodology for the deployment of formal verification which involves three complementary modes: architectural verification, block-level verification, and design exploration.     

构件组合的抽象精化验证

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.     

UML Statecharts的层次组合验证

该文在用层次自动机结构化表示UMLStatecharts的基础上,把Statecharts的层次结构特点纳入到组合验证中,使得对实现规范的验证可以通过把系统的某些层次精化部分用更抽象的规约代替来进行,以缓解模型检验中的状态爆炸问题。     

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

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

量子程序验证

量子硬件设计与制造技术的飞速发展使得人们开始预言大于一百个量子比特的特定用途的量子计算机有望在5-10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键.然而,由于量子信息的不可克隆性和纠缠的非局域作用等量子特征,如何设计正确高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法,特别是模型检测技术,已经在经典软件设计和系统建模方面被证明行之有效,因此量子软件的形式化验证也开始受到越来越多的关注.本文从量子顺序程序验证和量子通信协议验证两方面,对近年来国内外学者,特别是两位作者所在的研究组在该研究领域取得的一些成果进行了系统的总结.最后,对未来可能的研究方向和面临的挑战进行了简单展望.     

基于协议的实时构件行为一致性验证

对复杂实时构件系统行为进行形式化描述和一致性验证,可以提高实时构件的可复用性和系统的正确性、可靠性。分析了时间行为协议TBP(Timed Behavior Protocol)及其它学术界和工业界常用的时序行为形式化描述方法,对实时构件替换理论进行了讨论,给出了基于时间行为协议的构件一致性验证算法并对其进行了分析。     

基于SAT的软件验证

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.     

Bytecode Verification by Model Checking

Java bytecode verification is traditionally performed by using dataflow analysis. We investigate an alternative based on reducing bytecode verification to model checking. First, we analyze the complexity and scalability of this approach. We show experimentally that, despite an exponential worst-case time complexity, model checking type-correct bytecode using an explicit-state on-the-fly model checker is feasible in practice, and we give a theoretical account why this is the case. Second, we formalize our approach using Isabelle/HOL and prove its correctness. In doing so we build on the formalization of the Java Virtual Machine and dataflow analysis framework of Pusch and Nipkow and extend it to a more general framework for reasoning about model-checking-based analysis. Overall, our work constitutes the first comprehensive investigation of the theory and practice of bytecode verification by model checking. This revised version was published online in August 2006 with corrections to the Cover Date.     

面向特征编程范式的形式化验证技术研究综述

以面向对象编程范式开发软件经常面临类(Class)与用户需求项无法直接对应的尴尬,面向特征编程范式(FOP)旨在解决这个问题,因此具有重要意义。本文首先简介了FOP编程范式的思想,它与面向方面编程范式的异同,以及它给相应的形式化验证技术带来的挑战;然后综述了现有的FOP形式化验证方法以及我们所做的相关工作,比较了它们的优缺点;最后讨论了FOP形式化验证今后可能的研究方向。     

基于属性的访问控制策略的正确性验证

基于属性的访问控制策略以更精确的粒度控制着用户或进程对系统资源的访问,因此获得了越来越广泛的应用。然而必须保证所制定策略的正确性,才能防止对系统资源的非法访问,因此必须研制出一种有效的方法来验证策略的正确性。基于模型检测技术提出了一种访问控制策略的覆盖性与完整性验证方法。主要思想是将覆盖性与完整性验证归约为模型检测问题。将规则集与其变异分别视为模型,以模态逻辑公式描述其性质。调用模型检测算法,分别在模型及其变异模型上检测性质,生成反例报告以确定模型故障点和模型规则缺失点,同时分析性质本身的完善性,最终以完善后的模型和性质再次调用模型检测算法来完成覆盖性与完整性验证。实例分析结果表明覆盖性验证能够有效发现错误的规则,完整性验证能够有效识别验证规则的完备性。方法依托于模型检测工具完成,具有自动化程度高、易操作、测试结果可靠的特点。     

密码协议的一种安全模型

将密码协议与密码算法视为一个系统,建立了密码协议系统的一种安全模型.基于假设/保证的组合推理技术提出了新的假设/保证推理规则和假设/保证推理算法,证明了该规则的完备性,实现了密码协议系统的模型检查,并重点解决了系统分解问题、假设函数的设定问题、进程+逻辑的系统特性描述问题等难题.以kerberos密码协议系统为例,利用该安全模型和假设/保证推理技术对密码协议系统进行了安全验证.     

Verification of evolving software via component substitutability analysis

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning algorithm—previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the ComFoRT reasoning framework, and we report encouraging results on an industrial benchmark. This is an extended version of a paper, Dynamic Component Substitutability Analysis, published in the Proceedings of the Formal Methods 2005 Conference, Lecture Notes in Computer Science, vol. 3582, by the same authors. This research was sponsored by the National Science Foundation under grant nos. CNS-0411152, CCF-0429120, CCR-0121547, and CCR-0098072, the Semiconductor Research Corporation under grant no. TJ-1366, the US Army Research Office under grant no. DAAD19-01-1-0485, the Office of Naval Research under grant no. N00014-01-1-0796, the ICAST project and the Predictable Assembly from Certifiable Components (PACC) initiative at the Software Engineering Institute, Carnegie Mellon University. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the US government or any other entity.     

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

Symbolic Protocol Verification with Queue BDDs

Symbolic verification based on Binary Decision Diagrams (BDDs) has proven to be a powerful technique for ensuring the correctness of digital hardware. In contrast, BDDs have not caught on as widely for software verification, partly because the data types used in software are more complicated than those used in hardware. In this work, we propose an extension of BDDs for dealing with dynamic data structures. Specifically, we focus on queues, since they are commonly used in modeling communication protocols. We introduce Queue BDDs (QBDDs), which include all the power of BDDs while also providing an efficient representation of queue contents. Experimental results show that QBDDs are well-suited for the verification of communication protocols.     

基于符号模型检测的SDG故障诊断解形式化验证

由于定量信息和非线性因果关系的丢失,SDG的故障诊断解需要进一步的进行校核与验证。创新地将SDG故障诊断解的验证置于符号模型检测框架中进行研究,提出了基于符号模型检测的SDG故障诊断形式化验证方法。首先扩展、转换了SDG模型的有限状态变迁系统形式化描述,建立了SMV模型;其次引入故障传播时间建立了模型观测变量的动态验证信息,并基于步进式监控分析了动态验证策略,将SDG正向推理扩展建模为动态推理验证;然后面向符号模型检测扩展了动态推理验证过程的SMV模型,提出了验证算法SSDGFD_ SMC;最后,通过一个实例验证了算法的有效性。     

软件验证测试技术

软件验证技术是质量保证的重要手段,就其成就感和重要性来说,比确认测试有过之而无不及。测试小组通过软件审查和走查开展验证测试,开发验证"测试件",对各阶段文档形成通用审查单,使软件验证测试技术成为组织资产。它能够在开发早期发现缺陷,从而大大降低缺陷修复成本。     

IPv6邻居发现协议的形式化验证

采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.     

模式驱动的系统安全性设计的验证

随着万维网和移动计算技术的广泛应用,系统安全性得到了越来越多的关注,使用安全模式对系统安全解决方案进行设计并验证是提升系统安全性的一种有效途径。现有方法根据系统安全需求选择适用的安全模式,在此基础上将模式组合为系统的安全解决方案,并通过模型检测方法验证其安全性。但是,这些方法往往将方案看作整体进行验证,忽略了内部安全模式的组合细节,难以在包含大量模式的复杂系统中定位缺陷。提出一种模式驱动的系统安全性设计的验证方法,首先使用代数规约语言SOFIA描述安全模式及其组合,以构建系统安全解决方案的形式化模型;然后将SOFIA规约转换为Alloy规约后,使用模型检测工具验证模式组合的正确性和系统的安全性。案例研究表明,该方法能够有效地验证系统安全解决方案的正确性。