一种DDoS防御系统模型的设计研究

通过对当前DDoS现有防御策略的分析,提出基于分布式的检测,追踪和弱化的模型,简称DTM防御策略,并在此基础上设计一个具有增强功能的DDoS防御系统.     

分布式软件系统交互行为建模、验证与测试

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2．0序列图对模块之间交互行为进行描述．采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为 Promela 模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径．给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试．实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性．     

基于FDT技术的多总线集成研究与应用

针对现场总线系统中现场设备集成与系统集成问题,研究了FDT (field device tool)技术特点.在此基础上,将FDT技术应用到NCS4000系统中,以满足设备综合管理的需要,并提出了系统软件框架模型和系统集成模型.详细说明了网关DTM (device type manager)的实现方法,分析了DTM程序与现场设备的交互过程.通过开发DTM并将其集成到系统中,验证了设计的可行性.     

多核平台上一种分布式的虚拟运行环境

随着多核体系结构的快速发展,如何充分利用多核系统提供的计算能力,同时对可靠性、可扩展性和协同性提供支撑成为软件面临的难题。本文描述了一种运行在多核平台上的分布式虚拟运行环境DVRE,它为应用程序的有效运行提供支撑。DVRE在虚拟化技术的基础上以Client/Server的结构取代传统操作系统整体式的结构,以核之间通信的开销来取代操作系统中系统调用和上下文切换的开销,这种方法利用了多核平台高度的并行性,显示了良好的性能与可扩展性,同时DVRE底层的虚拟化机制提高了系统的可靠性与安全性。     

基于多接入点网络的集群防火墙系统设计

为解决分布式网络的安全策略问题,将安全检测在每个接入点上进行,防火墙模块间形成对等网络关系。在此基础上,提出一种基于多节点网络模型的集群防火墙系统设计方案,本系统采用模块化设计思想方法,实现了分布式环境下的安全数据的聚合,在实现传统状态检测技术的同时,又实现了分布式状态检测的基础策略,全面提高了防火墙系统的可用性、可控性、鲁棒性。     

在集群多核CPU环境下的等高线并行提取方法

分析集群环境下分布式存储编程模型和多核CPU环境下共享存储编程模型各自的优缺点,采用结合集群和多核CPU的并行环境来取长补短;并研究其在等高线提取中的相关并行算法,其中以建立三角网和跟踪等高线作为共享存储并行的研究实例;最后通过实验验证了该并行方案的可行性。     

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

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

一种分布式防火墙过滤策略的异常检测模型

分布式防火墙的安全性很大程度上取决于过滤策略正确配置。过滤策略的异常可能导致分布式防火墙系统所保护的网络出现严重的访问漏洞。为了能够自动化地检测分布式防火墙过滤策略存在的异常,对分布式防火墙系统中各过滤节点上的过滤规则之间可能出现的异常进行分类,并建立了一个过滤策略异常检测的模型。该模型能够检测出分布式防火墙过滤规则之间的冗余、冲突、不完整等各种异常,从而保证了分布式防火墙过滤策略的完整性和一致性。     

基于免疫代理的分布式入侵检测模型研究

随着计算机网络技术的迅速发展,网络安全也越来越引起重视,而入侵检测是当今研究的一个热点技术之一。然而,现今的分布式入侵检测系统还存在很多不足之处,如容错性、可靠性、协作能力以及可适应性等,本文讨论了一种基于代理的分布式入侵检测系统模型,并把免疫思想扩展到这个俣型框架之中。本文最终构造了一个基于免疫代理的分布式入侵检测模型框架。     

基于CR技术的OFDM有序分布小区资源分配算法

针对频谱资源紧张以及完全分布式网络需要自行组织、自主搜索从而开销很大的状况,提出一种将认知无线电技术应用于有序分布式网络的模型,并且提出分布式正三角形小区的调度算法和相应的子载波分配方案。该系统不仅可以充分利用子载波分集增益,提高系统容量,而且可以灵活地根据业务负载量选择使用其他覆盖区的子载波。仿真验证了所提算法的可行性,该模型有效提高了系统容量和频带利用率。     

软件动态调控策略的可信预评估模型研究

为了提高调控策略执行的成功率,提出以调控策略和其可信子属性为节点变量的贝叶斯网可信预评估模型,利用该模型对调控策略进行可信预评估。以电子交易系统为案例分析本方法的应用,并证实该方法的有效性。     

基于属性的支持策略本体推理的访问控制方法研究

基于属性的访问控制模型(ABAC)特别适用于大规模分布式网络。然而,由于网络环境的异构性以及策略控制的复杂性,其访问控制策略集往往庞大且缺乏统一语义,策略管理也因此变得复杂和易于出错。针对以上问题,使用本体一致性推理对现有的基于XACML的ABAC授权框架进行扩展:首先,对几种主要的访问控制模型在分布式环境下的性能进行量化分析;其次,通过对本体知识库的一致性检测来判断策略的一致性;最后,设计一个实验方案来验证该方法的有效性和正确性。     

基于IPC-PLC的海水提取硝酸钾网络化监控系统

根据海水提取硝酸钾的工艺控制要求和分布的地域特点，开发了由工业控制计算机和可编程控制器构成的分布式二级监控系统，并详细阐述了系统的软硬件构成以及控制策略的实现。经过实践运行表明，系统很好地满足了生产工艺的要求，完善了管理和控制功能，提高了生产效率，获得了较高的可靠性。     

Modeling and Analysis of Data Flow-Oriented ROS2 Data Distribution Service

Robot Operating System (ROS) is an open-source, meta-operating system, which can provide a structured communication layer based on the message mechanism on heterogeneous computing clusters. To improve the unsatisfactory real-time performance and reliability of data distribution in ROS1, ROS2 is proposed with a data flow-oriented data distribution service mechanism. This study validates the real-time performance and reliability of the ROS2 data distribution mechanism by means of probabilistic model checking. Firstly, a formal validation framework is put forward for the data flow-oriented ROS2 data distribution service system, and the probabilistic timed automata model is set up for the communication system module. Secondly, the probabilistic model checker PRISM is used to verify the real-time performance and reliability of data flow-oriented ROS2 data distribution service through the analysis of data loss rate and system response time. Finally, depending on the retransmission mechanism and Quality of Service (QoS) policy analysis, different data requirements and quantitative performance analysis of the transmission mode are achieved through the setting and adjustment of QoS parameters. This study can provide references for ROS2 application designers and the formal modeling, validation, and quantitative performance analysis of the distributed data distribution service based on the data flow.     

Model of distributed computing system operation with time

A mathematical model of the operation dynamics of distributed computing systems is presented. This model covers operation of both hardware and software components. The model provides a theoretical basis for performance, reliability, and consistency analysis, checking the correctness of operation, designing computing system architecture.     

基于体系结构模型检查分布式控制系统

分布控制系统是大量硬件设备通过计算机系统得以控制和协调的高度复杂系统,它们也是任务统,需要保障其功能的高度正确性和可靠性.分析复杂控制系统的过程包含了证明或验证设计的系统确实满足某种需求.但由于系统的复杂度,有效分析系统是相当困难的.从系统设计和分析的角度看,基于体系结构方法可以运用层次化构造和抽象的方法来减小模型复杂度.模型检查技术是分析复杂系统构造满足正确和可靠性需求的有效方法.结合软件体系结构描述方法和模型检查技术,提出了基于体系结构的分布式控制系统形式分析方法,通过楼宇综合控制系统实例研究,展示了该方法在提高分布式控制系统设计质量方面的效果.     

Stochastic game logic

Stochastic game logic (SGL) is a new temporal logic for multi-agent systems modeled by turn-based multi-player games with discrete transition probabilities. It combines features of alternating-time temporal logic (ATL), probabilistic computation tree logic and extended temporal logic. SGL contains an ATL-like modality to specify the individual cooperation and reaction facilities of agents in the multi-player game to enforce a certain winning objective. While the standard ATL modality states the existence of a strategy for a certain coalition of agents without restricting the range of strategies for the semantics of inner SGL formulae, we deal with a more general modality. It also requires the existence of a strategy for some coalition, but imposes some kind of strategy binding to inner SGL formulae. This paper presents the syntax and semantics of SGL and discusses its model checking problem for different types of strategies. The model checking problem of SGL turns out to be undecidable when dealing with the full class of history-dependent strategies. We show that the SGL model checking problem for memoryless deterministic strategies as well as the model checking problem of the qualitative fragment of SGL for memoryless randomized strategies is PSPACE-complete, and we establish a close link between natural syntactic fragments of SGL and the polynomial hierarchy. Further, we give a reduction from the SGL model checking problem under memoryless randomized strategies into the Tarski algebra which proves the problem to be in EXPSPACE.     

Kripke modelling and verification of temporal specifications of a multiple UAV system

A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke modelling is used to formally model the distributed cooperative control strategy, and to verify correctness of the specifications. Desirable properties of the mission such as liveness are specified in Computation Tree Logic (CTL). Model checking technique is used to exhaustively explore the state space to verify whether the system behaviour, modelled by Kripke model, satisfies the specifications. Violation of a specification is analysed by means of the counter-example generated by SMV model checking tool.     

基于可靠性理论的分布式系统脆弱性模型

对现有的脆弱性分析方法进行分析和比较,提出基于可靠性理论的分布式系统脆弱性模型.针对影响分布式系统安全性的各项因素进行脆弱性建模,利用模型检验方法构造系统的脆弱性状态图,描述系统脆弱性的完整利用过程,引入可靠性理论对分布式系统的脆弱性进行分析和量化评估,从而为增强分布式系统的安全性提供理论依据.     

Symbolic model checking for self-stabilizing algorithms

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors