广义不可推断属性符号化算术验证的研究

多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用.     

基于Petri网的信息流安全属性的分析与验证*

信息流安全属性的定义均基于不同的语义模型,很难作出比较,以Petri网作为描述安全系统的统一模型,在Petri网上定义四种常见的安全属性,并分析它们之间的逻辑关系。在信息流安全属性验证方面,传统的方法称为展开方法,该方法适用于确定型系统,而对于非确定型系统,该方法是可靠的,但不完备。进一步对Petri网上已经定义的四种属性给出可靠完备的验证算法,并开发出相应的验证工具。最后通过实例说明了验证方法在搜索隐通道方面的应用。     

不完备系统中一种增量式属性约简算法

实际应用中，信息系统的数据常常是动态变化的，当对象增加时，原始的属性约简集不一定有效。针对不完备决策系统对象增加的情况，提出基于条件熵的增量式属性约简算法。首先定义不完备决策系统中的条件熵，然后分析对象增加时条件熵的变化机制以及对约简集的影响，提出增量式属性约简算法，当对象增加时，该算法能够更高效地进行属性约简。最后，实验验证本文算法的有效性和高效性。     

信息量的不完备信息系统属性约简方法

针对不完备信息系统,提出一种基于信息量属性约简的新方法.该方法对传统的容差关系计算方法进行了改进,并在此基础之上给出了一种新的求核属性的方法.通过判断可以直接得到核属性,这样在计算的过程中大大的降低了属性约简算法的时间复杂度.最后设计了一个新的基于不完备信息系统信息量属性约简算法,通过实例验证了该算法的正确性、高效性.     

一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式,它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求,提出了对该模型进行形式化验证的算法：基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高可验证系统的规模.另外结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.     

变精度下不完备邻域决策系统的属性约简算法

邻域粗糙集模型在处理完备的数值型数据中得到广泛应用,但针对不完备的数值型和符号型混合数据进行属性约简的讨论相对较少。为此,首先结合邻域粗糙集给出了可变精度模型下不完备邻域决策系统的上、下近似算子及属性约简;然后通过邻域粒化的方法构建了广义邻域下可变精度的粗糙集模型,并提出了一种属性重要度的评价方法;在此基础上,设计出了面向不完备邻域决策系统的属性约简算法,该算法可直接处理不完备的数值型和符号型混合数据;最后,通过实例分析验证了本文提出的算法能够求解出变精度下不完备邻域决策系统的属性约简结果。     

基于分类质量的决策系统属性约简新算法

首先简要介绍几种决策表的属性约简算法,分析各种算法的优缺点,然后在此基础上提出一种新的属性约简算法——基于分类质量的决策系统属性约简算法。该算法对完备信息系统和不完备信息系统都是通用的,从其得到满意的属性约简,最后通过实例验证该算法的正确性和有效性。     

种基于监控理论的软件设计方法：状态性质变换方法

基于把离散事件系统监控理论用于软件设计的思想,本文中对软件设计的状态性质变换方法作了详细的讨论. 给定一个系统,其每一个状态的性质都是确定的. 当提出软件需求时,常常是对系统状态的性质提出需求.为设计出满足需求的系统,可以首先按照是否满足该性质对系统状态进行分类,再对不满足该性质的状态控制其可控事件的发生从而改变其性质使之满足要求的性质.本文将这种方法用于软件需求是不变性或可达性时的软件设计问题,通过和已有文献中结论的比较,显示了这种设计思想的广泛适用性和优点,也验证了软件控制论这一思想的可行性.     

不完备信息系统中基于限制容差关系的属性约简方法

决策表核属性的确定往往是信息约简的基础,然而以往的核属性约简方法大多是针对完备信息系统的。将完备信息系统中的属性核与属性序约简算法延伸至不完备系统,提出一种不完备信息系统中基于限制容差关系的属性约简方法。该方法通过构造限制容差关系下决策表的改进分辨矩阵来求得核属性,并将非核属性按直观影响分类质量的能力排序,能够保证得到的约简结果是相对最小约简。通过实验比较证明该方法可行、有效。     

基于聚类离散化和变精度邻域熵的属性约简

针对传感网采集数据的不完备性,利用数据本身特点,通过定义类簇指标,提出基于改进K-means聚类算法的数据离散化方法,以减小噪声、孤立点和不完备数据集对决策识别结果产生的影响;然后,通过引入互信息熵的属性重要度度量和变精度修正系数,提出基于互信息熵的变精度邻域粗糙集属性约简启发式算法,整合变精度和邻域粗糙集的优势,在减小约简算法计算复杂度的同时提高决策系统识别精度.仿真结果表明了算法在提高决策系统识别精度和降低其计算复杂度方面的有效性,模拟环境测试进一步验证了其工程适用性.     

Exact Acceleration of Real-Time Model Checking

Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and that can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effective. We illustrate our exact acceleration technique with run-time data obtained with the model checkers Uppaal and Kronos. Moreover, we demonstrate that automated application of our exact acceleration technique can significantly speed-up the verification of the run-time behavior of LEGO Mindstorms programs.     

BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

接口自动机的良构性检测算法及其实现

针对构件式系统中任一构件的非良构性会导致系统不能正常运行的问题,提出一种基于接口自动机（IA）来分析和检测构件良构性（well-formedness）的算法,并据此实现了一个构件良构性检测原型系统。该算法首先构造与接口自动机同构的可达图;其次,基于可达图通过深度优先遍历生成一条覆盖所有迁移的有序集;最后,根据该有序集检测在外界环境满足其输入假设的情况下,每个属于方法的活动到其对应返回活动的路径的自治无异常可达性,从而实现接口自动机的良构性检测。根据所提算法在Eclipse平台设计并实现了构件良构性检测原型系统T-CWFC,该系统通过JFLAP建立构件的接口自动机模型并构造其可达图,进而对接口自动机作良构性检测并输出相关检测信息。最后通过对一组构件的良构性检测实验验证了算法的有效性。     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

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.     

Checking timed automata for linear duration properties

It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M,An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes.Based on this,a method is proposed for checking whether M satisfies D.In some cases,the number of equivalence classes is too large for a computer to mainpulate,A technique for reducing the search-space for checking linear duration propoerty is also described.This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachablility analysis.     

基于场景规约的构件式系统设计分析与验证

使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.     

Regular Model Checking using Widening Techniques

In this paper, we consider symbolic model checking of safety properties of linear parametrized systems. Sets of configurations are represented by regular languages and actions by regular relations. Since the verification problem amounts to the computation of the reachability set, we focus on the computation of R^*(φ) for a regular relation R and a regular language φ. We present a technique called regular widening that allows, when it terminates, the computation of either the reachability set R^*(φ) of a system or the transitive closure R^* of a regular relation. We show that our method can be uniformly applied to several parametrized systems. Furthermore, we show that it is powerful enough to simulate some existing methods that compute either R^* or R^*(φ) for each R (resp. φ) belonging to a subclass of regular relations (resp. belonging to a subclass of regular languages).     

Model Checking for Hybrid Logic

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms.     

Relay Reachability Algorithm for Exploring Huge State Space

Since many desirable properties about finite-state model are expressed as a reachability problem, reachability algorithms have been extensively studied in model checking. On the other hand, reachability algorithms play an important role in game solving since reachability games are often described as a finite state model. In this sense, reachability algorithms are located in the intersection of the research areas of Model Checking and Artificial Intelligence.This paper interests in solving the reachability games called Push-Push. However, both exact and approximate reachability algorithms are not sufficient to the games since its state space is huge and requires lots of iterations such as 338 steps in the reachability computation. Thus we devise the new algorithm called relay reachability algorithm. It divides the global state space into several local ones. And exact reachability algorithm is applied on each local state space one by one. With these reachability algorithms, we solve all of the games.