基于反例确认的CPS不确定性模型校准

信息物理系统被广泛应用于众多关键领域,例如工业控制与智能制造.作为部署在这些关键领域中的系统,其系统质量尤为重要.然而,由于信息物理系统自身的复杂性以及系统中存在的不确定性（例如系统通过传感器感知环境时的偏差）,信息物理系统的质量保障面临巨大挑战.验证是保障系统质量的有效途径之一,基于系统模型与规约它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展,例如模型检验技术就被已用工作用于验证系统在不确定性影响下的行为是否满足性质规约,并在性质违反的情况给出具体的反例.这些验证工作的一个重要输入就是不确定性模型,它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事,因此验证中使用的不确定性模型很可能与实际不完全相符,这将导致验证结果不准确并与现实偏离.针对这一问题,本文提出了一种基于反例确认的不确定性模型校准方法,来进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准,并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索,最后结合假设检验来帮助决定是否接受校准后的结果.在代表案例上的实验结果表明了我们提出的不确定性模型校准方法的有效性.     

三值逻辑证明系统及正例与反例的提取

三值逻辑模型检验是对更高层的模型抽象验证的一种方法,对其验证中常常需要给出正例和反例.为此,讨论了三值逻辑模型检验以及正例和反例的提取,并在给出一套三值逻辑证明规则的基础上形成一个证明系统;运用该系统可以证明模型是否满足某个性质;在证明过程中为存在路径量词提取正例,为全称路径量词提取反例.正例和反例的提取可给模型的细化指明方向.最后通过实例给出了该证明系统在数字逻辑电路验证中的应用.     

基于CEGAR的Web应用验证

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.     

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

由于定量信息和非线性因果关系的丢失,符号有向图(SDG)的故障诊断解需要进一步进行校核与验证.将SDG故障诊断解的验证置于符号模型检测框架中进行研究,提出了基于符号模型检测的SDG故障诊断解形式化验证方法.首先定义了SDG模型的有限状态变迁系统形式化描述,建立了符号模型检测(SMV)模型;其次引入故障传播时间定义了模型观测变量的动态验证信息,提出了基于步进式监控的动态推理验证策略;然后扩展了动态推理验证过程的SMV模型,提出了验证算法SSDGFD_SMC;最后,通过一个简单贮水罐系统的SDG模型实例验证了算法SSDGFD_SMC的有效性.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

基于Horn逻辑扩展模型的安全协议反例的自动构造

根据安全协议的Horn逻辑扩展模型和相应的安全协议验证方法,提出了自动构造不满足安全性质的安全协议反例的求解策略,并给出了重要定理的证明,设计了一系列自动构造协议攻击的构造算法,并在基于函数式编程语言Objective Caml开发的安全协议验证工具SPVT中实现了这些算法,给出了主要算法的优化方法,详细分析了主要算法的时间复杂度,从理论上证明了算法是线性时间算法.最后,用SPVT对一些典型的安全协议进行了验证,得到了不安全协议的反例,并对反例进行了分析.得到的反例非常方便于阅读,与Alice-Bob标记非常接近,从而使任何领域的专家都可以用这种形式化的方法检查安全协议是否存在真实的反例.     

基于SPIN的地下建筑设备监控系统软件验证

在地下建筑智能化系统中,设备监控系统是基本的组成部分,其软件设计的正确性十分重要。提出了一种基于SPIN的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型,利用SPIN模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪,找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。     

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

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

在模型检验工具SMV中实现进程阻塞

模型检验技术是开发高可信软硬件系统的重要途径。目前已经有许多成熟的模型检验工具,SMV就是其中一种常用的工具,可以进行同步或异步系统的自动验证。在异步模型检验中,SMV可以描述进程,但不能直接描述进程的阻塞。本文提出了一种在SMV中利用公平性约束实现阻塞的方法。     

具体反例生成与图形化显示系统

模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法,模型检测相对于其它的模型检验方法有两个显著的特点,一个是它对模型进行检测的过程是自动化的,另一个是当系统不满足所验证的性质时,它会给出一条反例路径,这条反例路径可以为系统修正提供帮助．本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂,为系统修正带来更方便快捷的帮助．本文中实现了具体反例生成与图形化显示系统（简称CCGS）,它能快速生成离散语义下具体反例并图形化显示时间自动机沿着该具体反例的运行过程．实验结果表明CCGS能够快速生成具体反例路径信息,并且能够图形化显示具体反例信息,为系统修正提供更直观的信息,提高系统的正确性和安全性．     

Model checking large software specifications

In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems     

Kripke modelling and verification of temporal specifications of a multiple UAV system

A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke modelling is used to formally model the distributed cooperative control strategy, and to verify correctness of the specifications. Desirable properties of the mission such as liveness are specified in Computation Tree Logic (CTL). Model checking technique is used to exhaustively explore the state space to verify whether the system behaviour, modelled by Kripke model, satisfies the specifications. Violation of a specification is analysed by means of the counter-example generated by SMV model checking tool.     

On the expressiveness of the approach to constructing PLC-programs by LTL-specification

The article is devoted to an approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides a possibility of analysing the correctness of PLCprograms by using the model checking method. The linear temporal logic LTL is used as a language of specification of the program behavior. The correctness analysis of LTL-specification is automatically performed by the symbolic model checking tool Cadence SMV. The article demonstrates the consistency of the approach to constructing and verification of PLC programs by LTL-specification from the point of view of Turing power. It is proved that in accordance with this approach for any Minsky counter machine an LTL-specification can be built, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines are equipollent to Turing machines, and the considered approach also has the Turing power. The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting as a specific graphical language. ST is considered as a basic language because the implementation of a counter machine on IL, FBD/CFC and LD languages is reduced to rewriting blocks of an ST-program. The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.     

基于带参系统Murphi模型的SMV自动建模

提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快速不变式检查和限界模型检测等,但是建模过程复杂,模型不易维护.我们通过对两者进行分析,首先提出了能够很好描述带参系统的一个语义模型,然后读入相应的Murphi模型并进行分析以获取其语义模型表示,最后再通过一系列的策略自动得到限定参数时的SMV模型,由此得到的模型能够满足实际科研工作的应用要求.     

Construction and verification of PLC-programs by LTL-specification

An approach to construction and verification of PLC-programs for discrete problems is proposed. For the specification of program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLC-programs is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model. The purpose of the article is to describe an approach to programming PLC, which would provide the possibility of PLC-program correctness analysis by the model checking method. Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.     

TMN密码协议的SMV分析

MV是分析有限状态系统的一种工具,三方密码协议运行模式分析法是分析密码协议的有效方法之一,为了说明这种方法的可行性,使用三方密码协议运行模式分析法,并借助状态探测工具SMV分析了TMN密码协议,并成功地找到了对TMN协议的19种攻击。     

Verification of external specifications of reactive systems

External specification is currently approached by specification languages for describing and analyzing system requirements. The external specification can be defined during the early stages of the system development and can be very useful for: checking the class/system/subsystem requirements; checking the system composition; evaluating costs of reuse; defining validated reference requirements, histories, and traces for the final validation. The paper presents a collection of criteria in order to formally verify the external specification of reactive systems/subsystems. The verification criteria are grounded on the Tempo Reale object-oriented language (TROL) specification model for real-time systems. In TROL, the external specification is expressed in terms of ports and clauses with temporal constraints. The goal of the verification criteria presented is to check the completeness and consistency of the external specification with special attention to temporal constraints. These criteria can be applied to other real-time specification models and have been enforced in the tool object oriented machine state (TOOMS) tool. A practical example illustrates the verification process that embodies these criteria     

Formal semantics,modular specification,and symbolic verification of product-line behaviour

Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.     

基于模型检验的需求不一致研究

为在软件需求分析阶段获得易于理解且一致性需求,在现有的研究基础上,提出一种基于自然语言与模型检验相结合的方法.将自然语言描述的需求按照子句的相似度进行划分,提取关键词转换成自动机模型,对转换后的模型使用SM V语言描述并用模型检验工具和方法对模型进行分析和验证,通过乘坐电梯的案例对此方法进行实验验证.实验结果表明,该方...