自动生成参数化同步系统的符号化模型

验证具有任意进程个数的并发系统是一个重要的具有挑战性的课题。那些包含任意多个类似的有限状态进程的并发系统出现在一些领域中，如硬件设计、通信协议和高速缓存一致性协议。当验证进程数目较大的问题时，传统的有限状态验证技术遭受状态爆炸问题。为了解决这个问题，提出了一些不同的技术来推理无限家族，如互模拟关系、定理证明和网络语法、抽象解释和搜索技术。尽管在一般情况下，验证参数化并发系统是不可判定的，但对于一些包含相同的有限状态进程的子系统，已     

面向参数化系统验证的自动抽象方法

针对参数化系统验证面临的状态空间爆炸问题,提出自动抽象方法化简参数化系统状态空间.首先进行Y-抽象建立单进程有限状态机模型,然后通过对多个Y-抽象模型的合成运算得到异步合成的参数化系统,最后根据定义的谓词对参数化系统进行X-抽象得到二维抽象模型.运用该方法,对基于Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7个参数化协议和注入错误的MESI协议进行自动化抽象建模,并验证了相关性质,有效地提升了验证参数化系统的能力、缩短了验证时间;应用文中方法验证FT-1000CPU的一致性协议的结果表明,该方法在降低验证复杂度方面具有明显优势.     

嵌入式系统描述与验证环境的实现

首先，用统一建模语言(UML)中的状态图描述系统在整个活动周期中所处的不同的状态，活动图表示状态图中每个进程的功能，对象约束语言(OCL)描述系统中的约束条件；然后，用自行开发的软件UML2SC将UML描述的系统转换成SystemC代码，以完成系统的模拟验证；并介绍了该方法的一个应用实例。     

随机系统输出概率密度函数的有限时间镇定

针对一类含有限能量未知扰动的随机动态系统,研究基于随机分布函数的有限时间控制问题.通过B样条逼近建立了输出概率密度函数(PDF)与权值之间的对应关系,利用线性矩阵不等式,给出了基于观测器的PDF有限时间控制器的参数化设计方法.采用该方法设计的控制器,可使系统对所有满足条件的未知扰动是随机有限时间有界和随机有限时间镇定的.仿真实例验证了所提出方法的有效性.     

面向参数化LTL的预测监控器构造技术

介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称P_ALTL)公式运行时预测监控器构造方法.一方面研究P_ALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.     

乘性Markov 跳变系统鲁棒方差控制

针对一类具有乘性噪声和参数不确定性的Markov跳变参数系统,研究使得闭环系统的稳态状态方差小于某个给定的上界,同时满足一定H∞性能的状态反馈鲁棒方差控制器设计问题.运用线性矩阵不等式(LMI)方法,对系统进行了方差分析,给出并证明了控制器存在的条件,进而用一组线性矩阵不等式的可行解给出了控制器的一个参数化表示.最后的仿真结果验证了该方法的有效性.     

自动验证参数化Leader Election协议

讨论了一类Leader Election(LE)协议，该类协议通常运行在允许进程随时加入或崩溃的动态环境中，给出了LE协议的参数化版本，即考虑分布式系统中的进程数目任意多的情况。并提出了一种自动验证参数化LE协议的方法，用线性算数约束来模拟可能无限的全局状态集合，利用符号模型检测工具DMC[DP99]，文章实现了对参数化LE协议safety性质的自动验证。     

智能网业务逻辑的一种验证方法

智能网业务逻辑在不同的平面中有不同的表示。在总功能平面中,有一组总业务逻辑(GSL),它说明了完成各个业务独立模块(SIB)链接在一起的次序;在分布功能平面中,分布业务逻辑(DSL)是实现SIB功能时各个功能实体的动作和各个功能实体间的信息流;在物理平面中,包含业务控制功能(SCF)的物理实体执行业务逻辑程序。通信有限状态机模型是由表示进程的有限状态机和表示进程之间通道的先进先出队列(FIFO)组成。文章利用通信有限状态机(CFSM)模型描述智能网业务逻辑(SL),并给出了通过业务逻辑的CFSM模型验证业务逻辑正确性的一种方法。     

一类时滞组合系统的优化保成本容错控制

对一类时滞组合系统，研究了依赖时滞的分散状态反馈可靠保成本控制器的设计问题．采用线性矩阵不等式方法，导出了时滞依赖可靠保成本控制器的存在条件和参数化表示．进而，通过建立和求解一个线性矩阵不等式组约束的凸优化问题，给出了优化保成本容错控制器的设计方法．仿真实例验证了这个设计法的有效性．     

基于Mealy机的多主体演化博弈仿真研究

针对经济学研究中演化博弈建模表示与实现问题,提出构建一种基于Mealy有限自动机的经济学多主体博弈仿真系统.该系统用Mealy自限自动机表示组织和个人行为,采用面向对象的可视化界面控制技术构造有限自动机,利用人工智能中的语言翻译技术把有限自动机翻译成线程,并用并发调度和串行调度的方式对线程进行处理.在博弈过程中采用遗传算法产生新的有限自动机.用一个三人重复囚徒困境演化博弈实例,输入状态转换图,给出博弈均衡的结果.仿真实例表明系统方法是有效的.     

Covering sharing trees: a compact data structure for parameterized verification

The control state reachability problem is decidable for well-structured infinite-state systems like (Lossy) Petri Nets, Vector Addition Systems, and broadcast protocols. An abstract algorithm that solves the problem is the backward reachability algorithm of [1, 21 ]. The algorithm computes the closure of the predecessor operator with respect to a given upward-closed set of target states. When applied to this class of verification problems, symbolic model checkers based on constraints like [7, 26 ] suffer from the state explosion problem.In order to tackle this problem, in [13] we introduced a new data structure, called covering sharing trees, to represent in a compact way collections of infinite sets of system configurations. In this paper, we will study the theoretical complexity of the operations over covering sharing trees needed in symbolic model checking. We will also discuss several optimizations that can be used when dealing with Petri Nets. Among them, in [14] we introduced a new heuristic rule based on structural properties of Petri Nets that can be used to efficiently prune the search during symbolic backward exploration. The combination of these techniques allowed us to turn the abstract algorithm of [1, 21 ] into a practical method. We have evaluated the method on several finite-state and infinite-state examples taken from the literature [2, 18 , 20 , 30 ]. In this paper, we will compare the results we obtained in our experiments with those obtained using other finite and infinite-state verification tools.     

Heuristic search + local model checking in selective mu-calculus

Many tools for the automatic analysis or verification of finite-state distributed systems are based on construction of the global state graph of the system under consideration. Thus, they often fail because of the state explosion problem: the state space of a distributed system potentially increases exponentially in the number of its parallel components. To overcome this problem, we present a model checking procedure, based on the combination of heuristic searches with ideas taken from local model checking. We use heuristic mechanisms for exploration of the search space in order to avoid construction of the complete state graph.     

A New Approach to Upward-Closed Set Backward Reachability Analysis

In this paper we present a new framework for computing the backward reachability from an upward-closed set in a class of parameterized (i.e. infinite state) systems that includes broadcast protocols and petri nets. In contrast to the standard approach, which performs a single least fixpoint computation, we consecutively compute the finite state least fixpoint for constituents of increasing size, which allows us to employ binary decision diagram (BDD)-based symbolic model checking. In support of this framework, we prove necessary and sufficient conditions for convergence and intersection with the initial states, and provide an algorithm that uses BDDs as the underlying data structure. We give experimental results that demonstrate the existence of a petri net for which our algorithm is an order of magnitude faster than the standard approach, and speculate properties that might suggest which approach to apply.     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

基于吴方法的符号模型检验

模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而,随着系统规模的增大,BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题。     

Tree regular model checking: A simulation-based approach

Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. In this framework, the central problem is to compute the transitive closure of a transducer. Such a representation allows to compute the set of reachable states of the system and to detect loops between states. A main obstacle of this approach is that there exists many systems for which the reachable set of states is not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states, which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation, which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to various protocols.     

A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations

One of the best approaches for verifying software systems (especially safety critical systems) is the model checking in which all reachable states are generated from an initial state. All of these states are searched for errors or desirable patterns. However, the drawback for many real and complex systems is the state space explosion in which model checking cannot generate all the possible states. In this situation, designers can use refutation to check refusing a property rather than proving it. In refutation, it is very important to handle the state space for finding errors efficiently. In this paper, we propose an efficient solution to implement refutation in complex systems modeled by graph transformation. Since meta-heuristic algorithms are efficient solutions for searching in the problems with very large state spaces, we use them to find errors (e.g., deadlocks) in systems which cannot be verified through existing model checking approaches due to the state space explosion. To do so, we employ a Particle Swarm Optimization (PSO) algorithm to consider only a subset of states (called population) in each step of the algorithm. To increase the accuracy, we propose a hybrid algorithm using PSO and Gravitational Search Algorithm (GSA). The proposed approach is implemented in GROOVE, a toolset for designing and model checking graph transformation systems. The experiments show improved results in terms of accuracy, speed and memory usage in comparison with other existing approaches.     

Abstract reduction in directed model checking CCS processes

Model checking tools face a combinatorial blow up of the state-space (commonly known as the state explosion problem) that must be addressed to formally verify concurrent systems. We propose an approach combining abstraction techniques and heuristic search to overcome the problem above. In particular, heuristic search can avoid the bottleneck of the exhaustive exploration of the global state graph of a system, while retaining the advantages of abstraction techniques.     

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

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

Combining search space partition and abstraction for LTL model checking

The state space explosion problem is still the key obstacle for applying model checking to systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper presents an approach based on refinement of search space partition and abstraction which combines these two techniques for reducing the complexity of model checking. The refinement depends on the representation of each portion of search space. Especially, search space can be refined stepwise to get a better reduction. As reported in the case study, the integration of search space partition and abstraction improves the efficiency of verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.