基于多维度抽象和广度优先搜索空间划分的隐蔽信息流检测方法*

隐蔽信息流检测是开发可信计算机系统中的关键问题,而状态空间爆炸是基于状态机模型检测隐蔽信息流的主要障碍。提出一种多安全级系统中基于主体安全级的二维抽象方法,在此基础上设计了广度优先的搜索空间划分方法,使得划分变量的选取范围更大,扩展了搜索空间划分的应用范围,克服了深度优先划分方法中划分变量难以选取的问题。实验数据表明,结合抽象和搜索空间划分的方法有效降低了模型的验证规模,因此有效缓解了状态空间爆炸问题。     

平面离散点集的边界搜索算法

进行有限元仿真首先要建立有限元网格模型。使用不含有任何拓扑信息的离散点集直接进行网格划分可以快速、精确地建立网格模型。使用铺路法进行网格剖分是从边界开始向内生成网格单元。该文提出一种使用搜索盒的搜索平面离散点集边界的算法。该方法将离散点分配到搜索盒中，遍历位于边界的搜索盒，将其中的点连接成边界点链表。该算法能正确地搜索包含有凹点、孔洞特征的离散点集的边界，具有较强的通用性。文中介绍了算法的基本思想，并给出算例。     

基于物联网的系统差动保护方法实现

介绍了对未来可再生电能传输与管理系统保护及运行改进,该系统使用固态变压器连接住宅交流和直流微电网到配电系统,并使用故障隔离设备隔离故障线路,提出一种电流差动保护方案来检测基于FREEDM的微电网网络中的故障,该方法使用相量测量单元进行数据同步并最小化测量误差,并采用物联网技术和Wi-Fi通信方案在设备间进行数据监测和互连。然后通过一个仿真FREEDM系统进行测试,在不同位置施加了不同类型和不同故障电阻的故障来证明所提出的保护方法在检测故障状态方面的有效性,利用安全性、可靠性和准确性指标对所提出方法的性能进行了调查。最后设计、实施和测试了FREEDM系统的原型,使用Proteus软件模拟器和实验室进行了测试。测试结果证明,所提出的保护方案以快速、可靠和准确的方式检测和隔离故障状态的效率,该保护方案对于所有故障实现了高达98.825%的准确率。     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

电力无线专网中基于频谱检测的SDR技术

230 MHz电力无线专网系统作为目前电力负荷管理系统的主要构成部分之一,随着服务面的扩展和服务量的增大,传输速率低下、频谱资源浪费的缺点日益突出。频谱检测机制能够有效地搜索未使用的频谱空穴,而软件无线电可以充分利用检测到的频谱空穴并有效地提高频带利用率。提出了一种针对电力无线专网的基于频谱检测的软件无线电技术,结合电力无线专网230 MHz频段特点设计了通信系统中收发信机的数字电路,并通过MATLAB仿真验证了方案在在频谱检测上的性能表现。     

电台主控单元频率合成控制信号检测技术研究

为了对某型电台主控单元进行有效地测试,满足电台测试的迫切需求,提出了一种基于功能测试的检测方法,对主控单元输出控制信号进行检测,以判断其工作状态的好坏;通过对电路原理的分析,明确了控制信号的性能特征和参数指标;研究了检测整体思想和具体的检测技术和方法;详细介绍了检测过程中软件和硬件的设计思路和使用方法;实践表明,该方法能对主控单元时序信号进行有效的测试,软件设计有较好的通用性,能大幅提高电台主控单元测试水平.     

单元与网格选择技术在有限元分析中的应用

<正>本文结合SolidWorks Simulation软件中单元的技术特点与网格划分的规则,阐述了结构有限元分析中常见的单元类型和力学模型,并在此基础上讨论了仿真分析中单元的选取技术和网格的离散规则,为得到准确的有限元仿真结果提供了技术参考。     

基于动态克隆选择的入侵检测及其搜索核特征的研究

建立了一种基于动态克隆选择的入侵检测模型，结合模糊理论和统计方法，设计了一种新的检测器编码方式，通过划分子库、改进检测方法等途径对负向选择算法的伸缩性问题进行了探讨。文章首次提出了通过人工免疫的方法搜索入侵检测核特征的概念，并探讨了用本研究建立的入侵检测模型从候选特征中搜索核特征的方法。     

基于Petri网的密码协议形式化建模

密码协议是安全共享网络资源的机制和规范,是构建网络安全环境的基石,其安全性对整个网络环境的安全起着至关重要的作用。提出了采用Colored Petri Nets(CPN,着色Petri网)分析密码协议的新方法。采用新方法对TMN协议的多次并发会话通信进行形式化建模,模型依据会话配置和会话顺序进行功能单元划分,采用on-the-fly方法生成攻击路径。采用状态空间搜索技术,发现了该协议的多次并发会话不安全状态,并获得了新的攻击模式。     

LINUX进程间通信的模型检测

模型检测是一种强大的自动分析验证技术.分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案.     

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.     

Combining search space partition and 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 efficiencyof verification with respect to the requirement of memory and obtains significant advantage over the use of each of them in isolation.     

Distributed Branching Bisimulation Reduction of State Spaces

Enumerative model checking tools are limited by the size of the state space to which they can be applied. Reduction modulo branching bisimulation usually results in a much smaller state space and therefore enables model checking of much larger state spaces. We present an algorithm for reducing state spaces modulo branching bisimulation which is suitable for distributed implementation. The target architecture is a cluster with a high bandwidth interconnect. The algorithm is based on partition refinement and it works on transition systems which contain cycles of invisible steps, without eliminating strongly connected components first. To avoid fine grained parallelism, the algorithm refines the whole partition instead of just a single block in the partition. We prove correctness and also present some experimental results obtained with single threaded and distributed prototypes.     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

Partial-order reduction and trail improvement in directed model checking

In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking. We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking. Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples.     

SMT-based scenario verification for hybrid systems

Hybrid automata are a widely used framework to model complex critical systems, where continuous physical dynamics are combined with discrete transitions. The expressive power of Satisfiability Modulo Theories (SMT) solvers can be used to symbolically model networks of hybrid automata, using formulas in the theory of reals, and SAT-based verification algorithms, such as bounded model checking and k-induction, can be naturally lifted to the SMT case. In this paper, we tackle the important problem of scenario-based verification, i.e. checking if a network of hybrid automata accepts some desired interactions among the components, expressed as Message Sequence Charts (MSCs). We propose a novel approach, that exploits the structure of the scenario to partition and drive the search, both for bounded model checking and k-induction. We also show how to obtain information explaining the reasons for infeasibility in the case of invalid scenarios. The expressive power of the SMT framework allows us to exploit a local time semantics, where the timescales of the automata in the network are synchronized upon shared events. The approach fully leverages the advanced features of modern SMT solvers, such as incrementality, unsatisfiable core extraction, and interpolation. An experimental evaluation demonstrates the effectiveness of the approach in proving both feasibility and unfeasibility, and the adequacy of the automatically generated explanations.     

测试目的引导的模型检测方法与技术研究

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储。然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换。其次利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述。最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测并且可以缓解状态空间爆炸问题。     

Model Checking of Safety Properties

Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Proof rules for the verification of safety properties have been developed in the proof-based approach to verification, making verification of safety properties simpler than verification of general properties. In this paper we consider model checking of safety properties. A computation that violates a general linear property reaches a bad cycle, which witnesses the violation of the property. Accordingly, current methods and tools for model checking of linear properties are based on a search for bad cycles. A symbolic implementation of such a search involves the calculation of a nested fixed-point expression over the system's state space, and is often infeasible. Every computation that violates a safety property has a finite prefix along which the property is violated. We use this fact in order to base model checking of safety properties on a search for finite bad prefixes. Such a search can be performed using a simple forward or backward symbolic reachability check. A naive methodology that is based on such a search involves a construction of an automaton (or a tableau) that is doubly exponential in the property. We present an analysis of safety properties that enables us to prevent the doubly-exponential blow up and to use the same automaton used for model checking of general properties, replacing the search for bad cycles by a search for bad prefixes.     

Benchmarking Explicit State Parallel Model Checkers

This paper presents a set of benchmarks and metrics for performance reporting in explicit state parallel model checking algorithms. The benchmarks are selected for controllability, and the metrics are chosen to measure speedup and communication overhead. The benchmarks and metrics are used to compare two parallel model checking algorithms: partition and random walk. Implementations of the partition algorithm using synchronous and asynchronous communication are used. Metrics are reported for each benchmark and algorithm for up to 128 workstations using a network of dynamically loaded workstations. Empirical results show that load balancing becomes an issue for more than 32 workstations in the partition algorithm and that random walk is a reasonable, low overhead, approach for finding errors in large models. The synchronous implementation is consistently faster than the asynchronous. The benchmarks, metrics and results given here are intended to be a starting point for a larger discussion of performance reporting in parallel explicit state model checking.     

Directed explicit-state model checking in the validation of communication protocols

The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of naive search algorithms in the state space exploration.In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A^* directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations. We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search. We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A^* to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN. We provide experimental results from the protocol validation domain using HSF-SPIN.