一种状态事件故障树的时间特性分析方法

状态事件故障树是一种适合于描述构件化嵌入式系统失效因果链的建模技术,其顶层事件描述失效发生的结果.对顶层事件发生的平均时间进行分析,是获得系统平均失效时间参数的一种有效方法,可为系统的安全性评估提供支持.由于状态事件故障树缺乏严格语义,使得必须先对其进行形式化描述才能进行定量分析.为此,提出了一种基于交互马尔可夫链的状态事件故障树时间特性分析方法.首先,精化交互马尔可夫链的交互动作,建立接口交互马尔可夫链模型,并基于该模型对状态事件故障树的构件和逻辑门进行形式语义描述;其次,通过并行组合构件与逻辑门的形式语义模型,得到整个状态事件故障树的形式语义模型,并在该过程中使用弱互模拟对状态空间进行约简;然后,基于状态事件故障树的形式语义给出顶层事件发生的平均时间计算方法;最后,给出飞机着陆雷达控制系统和喷淋防火系统的状态事件故障树时间特性分析的实例研究.为构件化系统失效时间特性的分析提供了一种新方法.     

用时序和逻辑规则形成动态故障树的紧缩Markov链

针对枚举底事件的所有时序状态来形成Markov链的弊端,借鉴静态故障树的最小割集(minimum cut set, MCS)思想,考虑形成紧缩的Markov链（即最简顺序割集）。其重要目的是剔除冗余的Markov链,在保证不影响系统失效分析的同时减小状态空间,最大限度地避免陷入组合爆炸的危险。其显著特点在于用时序规则和逻辑规则来描述动态逻辑门。以此为基础,用BDD（binary decision diagram）技术首先形成基于逻辑规则的动态系统的MCS,其次对每个MCS运用时序规则,组合成必要的Mark     

一种基于UML类图和活动图的故障树生成方法

针对UML活动图在生成故障树的过程中只能反映活动事件流故障导致的系统失效,不能反映系统静态状态故障的问题,提出了一种活动图结合类图生成故障树的方法。在原有活动图的基础上,使用类图增加系统静态状态信息,设计活动图和类图到故障树模型的转换规则,将活动图中动态行为信息和类图静态状态信息转化为故障树中的节点要素。基于转换规则设计算法逆向遍历活动图和类图,自顶向下生成故障树。经过实例建模生成故障树,表明该方法能反映系统的动态行为和静态状态两方面的故障信息,为故障树生成提供了一种新的有效途径。     

动态故障树的边值多值决策图分析

动态故障树分析对于复杂系统来说是一种重要的可靠性分析技术,但是二叉决策图等传统模块化方法存在严重的状态空间爆炸问题.本文系统介绍了边值决策图的动态故障树分析方法,其中边值多值决策图相对于其它现有的决策图具有更紧凑的表示函数,通过状态数的缩减,缩短了计算时间,有效缓解状态空间爆炸问题.实例证明了边值多值决策图在多状态系统和多功能系统中使用的方法和优势.     

基于故障配置的故障树生成

故障树分析是提高系统安全性和可靠性的有效方法。传统的人工故障树生成方式难以解决当前系统的庞大规模与复杂性的问题,且容易出错。为此,提出基于故障配置的故障树生成方法,引入软件产品线的可变性管理,用于系统故障建模与形式化分析。首先,定义故障特征图模型用于刻画系统故障间的约束关系,基于Kripke结构定义故障标记迁移系统来描述系统的行为;然后,基于模型的语义建立通过模型检测生成故障树的过程;最后,通过时序逻辑描述系统安全属性,利用模型检测工具SNIP验证安全属性进而生成故障树。案例研究验证了该方法的有效性。     

基于贪心策略的多目标攻击图生成方法

为解决网络脆弱性分析中攻击图生成方法存在的状态组合爆炸问题,使生成的攻击图能用于网络中多个目标主机的脆弱性分析,本文提出了一种基于贪心策略的多目标攻击图生成方法。该方法引入节点关联关系,采用贪心策略精简漏洞集,从所有攻击路径中选取使攻击者以最大概率获取网络节点权限的攻击路径,生成由这些攻击路径所构成的攻击图。算法分析和实验结果表明,该方法的时间和空间复杂度都是网络节点数和节点关联关系数的多项式级别,较好地解决了状态组合爆炸的问题,生成的攻击图覆盖了攻击可达的所有节点,能够用于网络中多个目标主机的脆弱性分析。     

一种带有时间约束故障树分析方法

 在时间域内的行为对安全苛求系统往往是至关重要的,若出现故障,则大量的故障描述都涉及事件之间的时间因素。针对传统故障树不能直观描述和分析这种时间因素的问题,在原有故障树定义的基础上增加时间约束故障树的语义描述,并根据故障树的扩展语义提出时间约束故障树分析方法。给出时间约束逻辑门和事件平均转移率、输入事件到输出事件传播率和到达率的计算方法。设计故障树基本事件和最小割集到达顶事件的传播率和到达率的算法,该算法遍历故障树中每个节点获得基本事件时间重要度和最小割集到达率,从时间重要度角度对基本事件和最小割集的重要度比较。实验结果表明提出的时序分析方法可以为故障诊断和预防提供理论基础。     

基于増广Petri网生成受控日志

为减少冗余日志,降低事件约束不可控对算法评估及验证的影响,提出基于可达状态的随机选择生成受控日志的方法.利用増广Petri网为系统建立模型,依据模型中库所与变迁的结构关系及标识分布构建输入矩阵;基于Petri网可达状态分析方法,随机选择触发可发生变迁,记录变迁序列;对记录进行受控分析,拼装生成多重集事件日志和XES标准...     

基于多值决策图的动态故障树分析方法

针对具有动态故障模式的复杂系统,动态故障树分析一直是很重要的可靠性分析技术。为了提升可靠性分析效率,已有研究提出了各种模块化方法,但是对于实际动态故障树模型中由于事件关联导致的大型动态子树,这些模块化方法的状态空间爆炸问题仍然很突出。因此介绍了一种基于多值决策图(Multiple-valued Decision Diagrams,MDD)来分析动态故障树的方法,通过多值变量编码动态门,利用单一系统MDD模型刻画各种动态和静态可靠性行为,有效地缓解了状态爆炸问题。通过一个具体的实例说明了多值决策图方法的应用和优势。     

一种新的故障树定性分析方法

提出基于割序集的分析方法以研究故障树顶事件发生时基本事件的动态行为。利用顺序失效符表示事件的顺序失效关系,并将静态门和动态门转化为顺序失效表达式来描述故障树中各种门的动态行为,利用顺序失效表达式构建故障树的割序集。结合实例阐述故障树割序集生成算法的流程。该算法将失效行为表示为长度小于系统中部件个数的有序部件序列,为研究故障树提供了一种新的定性分析方法。     

Hierarchical reachability graph of bounded Petri nets forconcurrent-software analysis

Petri nets have been proposed as a promising tool for modeling and analyzing concurrent-software systems such as Ada programs and communication protocol software. Among analysis techniques available for Petri nets, the most general approach is to generate all possible states (markings) of the system in a form of a so-called reachability graph. However, this conventional reachability graph approach is inefficient or intractable, even for a bounded Petri net, due to state explosion in many practical applications. To cope with this problem, this paper proposes a method for constructing a hierarchically organized state space called the hierarchical reachability graph (HRG). Using the HRG, we obtain necessary and sufficient conditions for reachability and deadlock, as well as algorithms to test whether a given state or marking is reachable from the initial state and whether there is a deadlock state (a state with no successor states)     

Hierarchical Reachability Graph Generation for Petri Nets

Reachability analysis is the most general approach to the analysis of Petri nets. Due to the well-known problem of state-space explosion, generation of the reachability set and reachability graph with the known approaches often becomes intractable even for moderately sized nets. This paper presents a new method to generate and represent the reachability set and reachability graph of large Petri nets in a compositional and hierarchical way. The representation is related to previously known Kronecker-based representations, and contains the complete information about reachable markings and possible transitions. Consequently, all properties that it is possible for the reachability graph to decide can be decided using the Kronecker representation. The central idea of the new technique is a divide and conquer approach. Based on net-level results, nets are decomposed, and reachability graphs for parts are generated and combined. The whole approach can be realized in a completely automated way and has been integrated in a Petri net-based analysis tool.     

Past‐Free[ze] reachability analysis: reaching further with DAG‐directed exhaustive state‐space analysis

Model‐checking enables the automated formal verification of software systems through the explicit enumeration of all the reachable states. While this technique has been successfully applied to industrial systems, it suffers from the state‐space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. In this paper, we present a new reachability analysis algorithm, named Past‐Free[ze], that reduces the state‐space explosion problem by freeing parts of the state‐space from memory. This algorithm relies on the explicit isolation of the acyclic parts of the system before analysis. The parallel composition of these parts drives the reachability analysis, the core of all model‐checkers. During the execution, the past states of the system are freed from memory making room for more future states. To enable counter‐example construction, the past states can be stored on external storage. To show the effectiveness of the approach, the algorithm was implemented in the OBP Observation Engine and was evaluated both on a synthetic benchmark and on realistic case studies from automotive and aerospace domains. The benchmark, composed of 50 test cases, shows that in average, 75% of the state‐space can be dropped from memory thus enabling the exploration of up to 14 times more states than traditional approaches. Moreover, in some cases, the reachability analysis time can be reduced by up to 25%. In realistic settings, the use of Past‐Free[ze] enabled the exploration of a state‐space 4.5 times larger on the automotive case study, where almost 50% of the states are freed from memory. Moreover, this approach offers the possibility of analyzing an arbitrary number of interactions between the environment and the system‐under‐verification; for instance, in the case of the aerospace example, 1000 pilot/system interactions could be analyzed unraveling an 80 GB state‐space using only 10 GB of memory. Copyright © 2016 John Wiley & Sons, Ltd.     

State space analysis of Petri nets with relation-algebraic methods

A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net’s state space. Since state space explosion is still a serious problem, efficiently calculating, representing, and analysing the state space is mandatory. We propose a formal semantics of Petri nets based on executable relation-algebraic specifications. Thereupon, we suggest how to calculate the markings reachable from a given one simultaneously. We provide an efficient representation of reachability graphs and show in a correct-by-construction approach how to efficiently analyse their properties. Therewith we cover two aspects: modelling and model checking systems by means of one and the same logic-based approach. On a practical side, we explore the power and limits of relation-algebraic concepts for concurrent system analysis.     

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.     

EFSM最小可达图的同步生成算法

针对EFSM可达性分析过程中的状态空间爆炸问题,提出了一种基于变量值域划分的EFSM最小可达图的同步生成算法。该算法将EFSM可达图的生成与最小化两个过程结合在一起同步进行,引入特征配置的思想,依据特征配置指出变迁有效性组合,以及变迁的赋值动作与终止状态分组变量值域的关系,在进行可达性分析的同时仅对可达的状态分组进行稳定性判定及必要的分裂,直到所有可达状态分组均稳定为止,EFSM最小可达图即构造完毕。文中算法最大限度地减小了中间结果如不可达分组等对求解过程的影响,从而降低了传统算法因可达性分析与最小化过程相分离而引起的时间与空间上的巨大代价。     

基于极小T-不变量增加的Petri网可达性分析

基于极小T-不变量增加的Petri网的可达性分析,首先对网的状态方程加以合理的约束,求得一组特征解向量;然后利用扩展极小T-不变量关系图和扩展借矩阵在这些特征解向量的基础上适当添加整数倍的极小T-不变量;最后再判断这个添加极小T-不变量后的解向量的可达性。该方法不仅能判定一类含T-不变量Petri网的可达性,而且能在可达的情况下求得一个合法的变迁发生序列,并在一定程度上简化了可达性分析的过程。     

基于Petri网的工作流模型简化

计算状态空间可达图是验证工作流正确性的主要方法,状态空间爆炸是这类方法的主要困难.文章对线性时态逻辑LTL-x描述的正确性提出了一种基于Petri网图形化简的验证方法,证明了所提出化简规则的完备性,并以实例说明了所提方法的有效性.     

Construction of switching sequences for reachability realization of switched impulsive control systems

This paper studies the construction of switching sequences for reachability realization of switched impulsive control systems. An approach is proposed to design switching sequences so that the reachable subspace of switched impulsive control systems is expressed in terms of the reachable state sets of the designed switching sequences. For a class of switched impulsive control systems, it is proved that a single switching sequence can be designed with its reachable state set coinciding with the reachable subspace. Periodic switching sequences are also constructed in this paper for the reachability realization problem. The results present a new way to exploit the switching mechanism to achieve the reachability and controllability of switched impulsive control systems. Copyright © 2007 John Wiley & Sons, Ltd.