基于SMV的网络协议形式化分析与验证

提出了采用模型检验方法对网络协议进行形式化分析及自动验证，建立了一个特定网络协议PAR的有限状态机模型，并用模型检验工具SMV验证其正确性，发现了该协议存在的一些缺陷。结果表明，利用符号模型检验方法分析检验网络协议是可行的。     

模型检验软件体系结构研究与进展

软件体系结构经过10多年的发展，在体系结构的基础理论、体系结构风格、体系结构描述语言和体系结构建模等方面的研究取得了一系列可喜的成就。目前，就软件体系结构的分析、评价、测试和验证的研究也在如火如荼地进行中。模型检验是一种基于自动机理论的形式验证方法，采用穷举状态空间的方式来证明系统的模型是否满足要验证的属性。同传统的测试和验证的手段相比，模型检验有其自身的优势。为此，越来越多的研究人员正在将模型检验技术应用到软件体系结构的分析和验证中。本文调查了模型检验技术在软件体系结构中的应用现状，剖析了影响软件体系结构模型检验的因素，给出了软件体系结构模型检验的未来主题。     

基于事件图的离散事件仿真模型并行检验方法

非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.     

基于LSC的模型检验研究

LSC是一种表达能力很强的顺序图建模语言，模型检验技术是验证软件模型正确性的重要方法，提出了一个对LSC模型进行模型检验的方法，并实现了相关支持工具。首先分析了LSC语言，然后基于其语义提出了生成LSC等价状态模型的方法，进而对生成的状态模型进行模型检验；最后进行了实例研究，利用给出的实现工具检验了用CTL描述的验证性质。     

异步FIFO的模型检验方法

跨时钟域(Clock Domain Crossing,CDC)设计和验证是SOC系统芯片设计的关键问题。讨论了异步FIFO的模型检验方法,利用模型检验工具SMV,建立了异步FIFO的有限状态机模型,使用时序逻辑LTL对该模型和属性进行了描述和验证。实验结果达到要求,同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较,模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。     

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

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

基于交互式马尔可夫链的模型检验

研究了基于交互式马尔可夫链（IMC)的模型检验,IMC是集功能描述和性能刻画为一体的并发系统模型,模型检验是一种自动功能验证与性能评价技术。文中提出的模型检验算法结合了传统的功能验证与性能评价的功能,并且与现有的算法相一致。实验分析表明,该算法具有较高的性能,适用于大型复杂系统的验证和评价。     

模型检验在航天测控软件上的应用研究

模型检验是确保程序质量的有效手段,能弥补软件测试的不足。但航天测控软件规模大、输入数据复杂、验证性质不明确等因素极大地阻碍了模型检验的应用。针对航天测控软件,分析了其特点以及对其执行模型检验的困难,提出了基于有界模型检验器CBMC的模型检验应用框架,包括航天测控数据的构造方法及验证性质的提取方法。随后,将该框架应用于外测数据处理软件,取得了良好的效果。     

并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

并发和实时系统的模型检验技术

模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态／命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。     

软件验证与确认在MIS开发中的应用

介绍软件验证和软件确认的概念及其相互关系,以一个实际的管理信息系统开发项目为例,描述在软件开发生命周期中验证和确认活动的具体实现,以及如何使验证和确认与项目的整个生命周期相配合、如何与项目实体相关联,证明软件验证和确认是保证软件产品质量的有效手段.     

Application of a Methodology for the Development and Validation of Reliable Process Control Software

This paper discusses the necessity of a good methodology for the development of reliable software, especialy with respect to the final software validation and testing activities. A formal specification development and validation methodology is proposed. This methodology has been applied to the development and validation of a pilot software, incorporating typical features of critical software for nuclear power plant safety protection. The main features of the approach indude the use of a formal specification language and the independent development of two sets of specifications. Analyses on the specifications consists of three-parts: validation against the functional requirements consistency and integrity of the specifications, and dual specification comparison based on a high-level symbolic execution technique. Dual design, implementation, and testing are performed. Automated tools to facilitate the validation and testing activities are developed to support the methodology. These includes the symbolic executor and test data generator/dual program monitor system. The experiences of applying the methodology to the pilot software are discussed, and the impact on the quality of the software is assessed.     

A PASCAL validation office

A PASCAL validation office is presented as a key element in the development of portable software. A number of software portability issues are briefly surveyed as well as problems involved by the definition of programming language standards. The validation office is used for both the technical aspects of compiler testing and the organization aspects of validation procedures.     

面向机载软件的预期功能安全分析验证过程及方法研究

预期功能安全（Safety of the Intended Functionality,SOTIF）关注系统与外界环境、交联设备、任务场景和操作人员交互时,由自身功能设计不足而导致的安全隐患,非常适用于具有复杂功能逻辑的系统和软件研制过程。但目前尚未见到SOTIF在机载软件安全性分析验证工作中的研究与应用,导致机载软件安全性分析验证过程难以适用于复杂失效的分析识别。因此借鉴SOTIF在汽车领域的成功应用经验,开展面向机载软件的SOTIF分析验证过程与方法研究。首先,参考ISO 21448标准,提出机载软件SOTIF分析验证框架。然后,借助功能危险分析、故障树模型、场景驱动等理论,针对过程中涉及的SOTIF分析验证技术进行研究,识别机载系统危险,分析软件异常控制行为及其原因,构建SOTIF测试场景与测试用例,形成基于SOTIF的机载软件安全性分析验证完整闭环。最后,通过SOTIF技术在机轮转弯控制软件的典型工程应用,验证了该研究成果的有效性和可行性,形成了面向机载软件的SOTIF分析验证过程与能力,可支撑研制人员充分识别机载软件运行过程中软硬耦合冲突、人机交互异常、场景切换异常等复杂失效模式,确保机载软件满足高安全、高可靠研制要求。     

An acyclic expansion algorithm for fast protocol validation

For the development of communications software composed of many modules, protocol validation is considered essential to detect errors in the interactions among the modules. Protocol validation techniques previously proposed have required validation time that is too long for many actual protocols. The authors propose a novel fast protocol validation technique to overcome this drawback. The proposed technique is to construct the minimum acyclic form of state transitions in individual processes of the protocol, and to detect protocol errors such as system deadlocks and channel overflows fast. The authors also present a protocol validation system based on the technique to confirm its feasibility and show validation results for some actual protocols. As a result, the protocol validation system is expected to improve productivity in the development and maintenance of communications software     

A formal methodology using attributed grammars for multiprocessing-system software development II. Validation

Validation of large-scale software is frequently complicated by the need to ensure proper synchronization among concurrent processes in multiprocessing systems. The validation method presented is based on the use of a model using attributed grammars for specifying the control and data flows of the system. In paper I, a method of deriving the model was presented. In this paper, the model is used for generation of test cases and for validation of the implemented software system. This approach is especially significant because a common model is used for both design analysis and validation for multiprocessing-system software.     

基于SSL的软件序列号网上验证分析与实现

在软件序列号网上验证过程中,若数据为明文传输的话,则容易被捕获及分析,从而令验证失效。为降低软件盗版比例,介绍序列号验证技术的基本原理,通过实例详细说明利用SSL加密验证过程的必要性,给出获取SSL服务器证书的不同途径,利用Windows HTTP服务（WinHTTP）为软件开发人员提供解决方案。提出的方法有效、实用且易于实现。     

Validation of software in measuring instruments

Most measuring instruments of today are based on embedded systems or personal computers. The software embedded into the instruments controls functions that must be possible to verify and validate. Validation of software is certainly performed by the developing companies, but also the independent test laboratories must be able to perform the validation. Traditional evaluation of measuring accuracy and resistance to environmental stress is not enough to confirm the functionality of the instrument.An efficient validation procedure often combines different kinds of validation methods. The set of validation methods can be collected as a “tool box” which can be applied differently for different measuring instruments. The risk classes, the validation guidance and some possible validation methods are discussed. The paper is based on the work carried out by the European project “MID-Software”.     

核电厂DCS安全级应用软件开发的危险分析

为了减小或避免因控制系统软件而导致的核电厂安全性降低的不良后果,提出了对核电厂数字控制系统安全级应用软件开发过程进行危险分析的活动.采用验证和确认的方法,并结合安全保护层模型、预先危险分析方法(PHA)、故障树分析等方法对应用软件开发过程中的系统设计、软件设计、软件实现各个阶段的危险进行分析.通过CPR1000项目工程实践表明,采用验证和确认的方法能有效地减小软件开发过程中的危险以提高应用软件的安全性,从而最终提高核电厂的安全性.     

Relating software validation to technology trends

Large scale software engineering is undergoing substantial shifts due to a combination of technological and economic developments. These include the prevalence of software for embedded systems, global software development across geographically distributed teams, the technological shift towards multi-core platforms, and the inevitable shift towards software being used as a service. In this overview article, we discuss some of the challenges that lie ahead for software validation, due to such technological developments. In particular, we provide a brief introduction to the papers appearing in this special issue, many of which specifically focus on validation of software running on real-time embedded systems.