广义可能性决策过程的计算树逻辑模型检测

模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。     

具有多值决策过程的广义可能性计算树逻辑模型检测

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。     

具有DP的广义可能性模糊时态CTL模型检测

为了增强计算树逻辑在时序上的表达能力,以广义可能性测度、决策过程和计算树逻辑为基础,研究了具有决策过程的广义可能性模糊时态计算树逻辑的模型检测。首先采用广义可能性决策过程作为系统模型;然后引入模糊时态算子,构造了模糊时态计算树逻辑并给出其在广义可能性测度下的语义,得到新的广义可能性模糊时态计算树逻辑用来描述系统属性;最后在广义可能性调度下通过模糊矩阵运算讨论了"soon、within、last、nearly"等几类模糊时态连接词的具体计算方法,给出相应的模型检测算法。经验证明,广义可能性模糊时态计算树逻辑是广义可能性计算树逻辑在模糊时序上的扩充,具有更强的表达能力。     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

基于符号化模型检测的对弈必胜策略验证

在对弈的研究中,验证对弈双方是否存在必胜策略的问题一直没能很好地解决,因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展,大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法,并给出了一个井字棋必胜策略验证的实例。     

不确定环境下基于VaR和CVaR的投资组合优化模型

对不确定环境下的投资组合问题进行研究,使用不确定测度来定义不确定环境下的VaR和CVaR,并用VaR和CVaR度量风险,建立基于VaR和CVaR风险控制的投资组合优化模型,并设计了集成遗传算法、99-方法的混合智能算法来求解此模型,最后通过实例验证了模型和算法的有效性。     

供应链库存的模糊机会约束规划模型

研究了不确定环境下的供应链库存优化问题。考虑需求为模糊量,且可能在一定条件下不满足约束条件的决策前提,用三角模糊数表示需求,结合可能性理论中的可信性测度,建立了多品种联合补充的模糊机会约束规划模型,目标函数为最小化供应链订货成本和库存成本的期望值。用遗传算法对优化模型求解,以目标函数值作为染色体适应度,给出了编码方案及选择、交叉、变异算子。用数值实例进行了仿真计算,证明了模型和算法的有效性和性能,并给出了不同置信水平下的计算结果。     

基于深度学习算法的风电机组叶片开裂缺陷分析

为实现对风电机组叶片表面缺陷检测的智能化,本研究应用无人机技术、图像视觉技术和深度学习算法,建立风电机组叶片缺陷检测系统,提高了对叶片上开裂缺陷的检测精度。系统使用 算子计算图像横向和纵向的梯度,并对图像进行阈值分割和去噪处理。构建深度学习模型提取图像缺陷的特征信息,加入了SPP-Net网络进行卷积操作,增加了模型的输入数据尺度,得到特征图后在利用PRN网络筛选特征图。实验结果显示本研究系统能够去除大量无用的背景信息,开裂缺陷部位的特征信息保留完整,对验证集中的图像进行测试后,本研究系统识别出的开裂缺陷数最高可达到50个。     

符号化模型检测CTL

提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的.     

面向CPS复杂事件流的不确定性研究

信息物理融合系统CPS获得广泛应用需要解决的一个关键问题是软件中的信息处理部分,而复杂事件处理是CPS中信息处理的核心任务之一。CPS环境下的事件具有异构、分散、海量和不确定性等特征。在CPS实际应用中,因噪声、传感器误差、通讯技术等原因而造成的事件不确定性急需解决。为了解决CPS系统中存在的海量不确定事件流问题,提出一种处理不确定事件流的复杂事件处理方法USCEP,该方法不仅可以实时有效地处理海量不确定事件流,还可以有效计算复杂事件的概率。USCEP对现有RFID复杂事件监测方法 RCEDA进行了改进,提供了历史概率事件查询处理的支持,提出一种事件概率模型进行概率计算,并通过关联查询表来提高效率。实验表明,在处理不确定事件流时,该方法比传统方法具有更好的性能。     

Symbolic Verification and Analysis of Discrete Timed Systems

This paper presents a novel approach for real-time model checking. It combines the efficiency of traditional symbolic model checking with possibilities to describe and specify real-time systems. Using multi-terminal binary decision diagrams to represent time and time intervals, it becomes possible to transfer efficient algorithms and optimization heuristics known from standard CTL model checking to real-time applications. By introducing a new variant of models called I/O-interval structures we can describe systems in a modular way. Interval structures allow model composition of real-time structures such that state explosion effects are greatly reduced. Besides model checking we also present analysis algorithms which allow to compute key properties like system latencies and minimal response times from the structures describing the system. The practical applicability is proven by experimental results, computed by the verification system RAVEN, which implements all described algorithms, including counterexample generation and waveform visualization.     

Bisimulation Minimization and Symbolic Model Checking

State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.     

An environment for formal verification based on symbolic computations

We present an environment for formally verifying hardware, based on symbolic computations. This includes a new concurrency model, called the combinational/sequential or C/S concurrency model which has close ties to hardware. We allow fairness constraints and describe methods for specifying them and for formally verifying in their presence. Properties are specified by either CTL formulae or edge-Rabin automata. We give algorithms, in the presence of fairness constraints, for model checking CTL or for checking that the language of our system is contained in the language of a property automation. Finally, techniques are given for hierarchical verification and for detecting errors quickly (early failure detection).     

计算树逻辑特性模式研究

模型检查是系统验证的有效方法,在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画,然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义,根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式,包括缺失性模式、存在性模式、普遍性模式、优先性模式和跟随性模式等。     

Optimizing symbolic model checking for statecharts

Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic modal checking for systems specified as statecharts. We used these techniques in our analyses of the models of a collision avoidance system and a fault-tolerant electrical power distribution (EPD) system, both used on commercial aircraft. The techniques together reduce the time and space requirements by orders of magnitude, making feasible some analysis that was previously intractable. We also elaborate on the results of verifying the EPD model. The analysis disclosed subtle modeling and logical flaws not found by simulation     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

Module Checking

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.     

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

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

Model checking probabilistic social commitments for intelligent agent communication

Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent communication. They exploit observable social commitments to develop a verifiable formal semantics through which communication protocols can be specified. Developing and implementing algorithmic model checking for social commitments have been recently addressed. However, model checking social commitments in the presence of uncertainty is yet to be investigated.In this paper, we propose a model checking technique for verifying social commitments in uncertain settings. Social commitments are specified in a modal logical language called Probabilistic Computation Tree Logic of Commitments (PCTLC). The modal logic PCTLC extends PCTL, the probabilistic extension of CTL, with modalities for commitments and their fulfillments. The proposed verification method is a reduction-based model checking technique to the model checking of PCTL. The technique is based upon a set of reduction rules that translate PCTLC formulae to PCTL formulae to take benefit of existing model checkers such as PRISM. Proofs that confirm the soundness of the reduction technique are presented. We also present rules that transform our new version of interpreted systems into models of Markov Decision Processes (MDPs) to be suitable for the PRISM tool. We implemented our approach on top of the PRISM model checker and verified some given properties for the Oblivious Transfer Protocol from the cryptography domain. Our simulation demonstrates the effectiveness of our approach in verifying and model checking social commitments in the presence of uncertainty. We believe that the proposed formal verification technique will advance the literature of social commitments in such a way that not only representing social commitments in uncertain settings is doable, but also verifying them in such settings becomes achievable.