基于SPN的信息系统生存性分析建模研究

研究基于随机Petri网(SPN)的信息系统生存性分析建模方法.首先,将信息系统抽象为请求组件、通信组件、处理组件和存储组件4个部分;其次,将信息系统工作流程形式化描述和生存性分析建模相结合,并分别描述了通用信息系统、系统组件失效修复、串联并接、冗余以及具有可生存属性组件的随机Petri网建模方法.从而对系统形式化描述的同时对系统生存性能做了定性和定量分析;最后,仿真实验证明基于SPN建模方法分析信息系统生存性的有效性和准确性,并为可生存的信息系统设计提供理论基础和指导.     

面向容侵系统可生存性量化的随机博弈模型研究

提出面向生存性研究的容侵系统状态转换模型,提高对容侵过程的描述能力,将入侵者和入侵容忍系统作为随机博弈的局中人,建立了描述入侵过程的随机博弈模型,使用纳什均衡计算了博弈结果,使用基于连续马尔可夫过程的方法对容侵系统可生存性进行了量化评估.最后,利用博弈分析的结果和所建立的评估模型进行了容侵系统的生存性分析,指出了容侵系统生存性敏感的参数.     

网络信息系统生存性层次化分析模型研究

为了保障网络系统在面临攻击的时候能够稳定、可靠地提供服务,必须考虑网络系统自身的生存能力.分析影响网络系统生存性的首要因素是系统存在漏洞,而服务质量变化是系统生存性降低的外在表现形式.提出一种基于网络攻击图原理的层次化系统可生存性量化评估模型,该模型根据系统中关键服务及其原子服务组件信息,进行漏洞探测,生成网络攻击图和攻击方案,并对系统进行基于真实环境下的生存性测试,记录攻击中和攻击后的服务质量变化.通过服务质量变化分析系统生存性的四个关键属性(3R A),最终实现对整个网络系统的生存性量化分析,并通过实验验证了该模型的有效性和准确性.     

一种移动Ad Hoc网络可生存性模型建模及仿真验证方法

针对网络可生存性模型考虑因素不同、模型描述各异和实验环境概念不同所造成的彼此之间较难的可比性问题,文中提出了一种用于评判多种移动Ad Hoc网络可生存性模型的建模及其仿真验证方法.从可生存性定义出发,采用本体构建可生存性模型的高层描述,在此基础上研究了高层描述向低层仿真执行的转换技术,提出了基于攻击路径自动生成的防御仿真任务部署方法,并实现了可生存性模型的仿真验证.最终在面向战术环境的移动Ad Hoc网络中,通过对SAMNAR模型和群组恢复模型的建模验证说明了文中方法的有效性.     

基于支持向量数据描述的网络可生存性综合评估

针对网络可生存性综合评估方法中指标权重难以确定的问题,提出了基于支持向量数据描述(SVDD)的网络可生存性综合评估方法。该方法分析了SVDD的几何意义,采用二进制粒子群(BPSO)算法对建立的评估特征指标集进行特征选择,将所得的特征指标集视为整体来建立SVDD分类模型,并以测试样本点与模型的相对距离为依据评估系统的可生存性,避免了综合评估中指标权重确定的主观性。最后通过网络实例验证了评估模型的有效性。     

基于随机Petri网的电信交换系统可生存性分析

网络系统的可生存性问题是系统安全领域的一个重点研究方向。讨论现有的系统可生存性的一般分析方法,确定系统的可生存属性,并采用随机Petri网(SPN)技术,分析电信交换系统生存性问题的特点。重点利用随机Petri网描述系统的失效-修复分析模型和性能分析模型,给出系统可生存性分析中主要指标的定量计算方法。系统仿真结果表明了该方法的有效、合理性。     

可生存性分析方法研究

系统在受到入侵后依然能够提供必要服务,并在一定时间内恢复受侵害的服务是系统可生存性的本质要求,与传统的将可生存性作为非功能系统属性描述的方法不同,将可生存性作为系统统一系统功能来研究,并用形式化语言来描述,定义和计算是一种全的思路和方法,对可生存性分析阶段可以采用的方法进行了深入的研究,分析,其中重点阐述了工作流回溯,攻击树建立等可生存性需求分析的方法,并给出了可生存性量化分析的算法。     

基于状态转换的信息服务系统可生存性评估方法

可生存性评估是使用各种方法对目标系统进行定性及定量的生存性分析。本文提出了一个基于状态转换的信息服务系统可生存性评估方法,该方法包括一个系统生存性模型和一个生存性函数的定义。最后给出了使用这种评估方法对目标系统进行评估的实例。     

高性能开放式数控系统框架设计

描述一个高性能开放式数控系统结构框架.该框架采用基于功能组件的厂商无关结构,通过绑定表(binding table)方式,支持组件功能的软硬件协同实现.本框架引入实时交互网络中(RTN)中的异步通讯机制(ACM)为整个系统提供统一的通讯模型,并设计相应的功能组件.在统一通讯模型支持下,该框架支持数控系统采用一个或者多个处理器或控制器的分布式结构,满足日益增长的数控系统高性能要求.本文基于该框架实现了原型系统.     

基于随机博弈的网络可生存性策略选择模型

为了提高网络的可生存能力,提出了基于随机博弈的网络可生存性策略选择模型。该模型针对攻击和破坏行为对网络造成的影响,将攻防双方的博弈过程分为抵抗、识别和恢复三个阶段。从细节上描述系统状态转移与策略选择之间的关系,提出了基于上述模型的策略选择分析方法。最后以网络实例表明了该模型在预测攻击行为并选取最优可生存性策略方面的可行性和有效性。     

Bi-Decomposition of Function Sets in Multiple-Valued Logic for Circuit Design and Data Mining

This article presents a theory for the bi-decomposition of functions in multi-valued logic (MVL). MVL functions are applied in logic design of multi-valued circuits and machine learning applications. Bi-decomposition is a method to decompose a function into two decomposition functions that are connected by a two-input operator called gate. Each of the decomposition functions depends on fewer variables than the original function. Recursive bi-decomposition represents a function as a structure of interconnected gates. For logic synthesis, the type of the gate can be chosen so that it has an efficient hardware representation. For machine learning, gates are selected to represent simple and understandable classification rules. Algorithms are presented for non-disjoint bi-decomposition, where the decomposition functions may share variables with each other. Bi-decomposition is discussed for the min- and max-operators. To describe the MVL bi-decomposition theory, the notion of incompletely specified functions is generalized to function intervals. The application of MVL differential calculus leads to particular efficient algorithms. To ensure complete recursive decomposition, separation is introduced as a new concept to simplify non-decomposable functions. Multi-decomposition is presented as an example of separation. The decomposition algorithms are implemented in a decomposition system called YADE. MVL test functions from logic synthesis and machine learning applications are decomposed. The results are compared to other decomposers. It is verified that YADE finds decompositions of superior quality by bi-decomposition of MVL function sets.     

Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.     

一种用于实现任意基数值时序逻辑的阈值存储电路

本文基于多值时序电路的次态方程和输出方程最小项展开式,提出了一种具有任意值输入、双轨二值输出的阈值存储电路设计方案,它和多值与或门配合,运用Disjoint代数能够设计出任意基数值时序电路.文中通过三值九进制计数器的设计,阐明了任意基数值时序电路的设计方法.     

A multiple valued logic: a tutorial and appreciation

This tutorial places the developments and potential of multiple-valued signals and logic in the relevant context of binary and two-valued signals. It covers: the role of multivalued logic (MVL) in the binary world; multivalued representation; binary-related radices; multivalued functions; storage techniques in MVL; and implementation issues. An overview of applications is included     

基于模型检测的系统生存性分析

提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。     

A novel ternary half adder and multiplier based on carbon nanotube field effect transistors

A lot of research has been done on multiple-valued logic (MVL) such as ternary logic in these years. MVL reduces the number of necessary operations and also decreases the chip area that would be used. Carbon nanotube field effect transistors (CNTFETs) are considered a viable alternative for silicon transistors (MOSFETs). Combining carbon nanotube transistors and MVL can produce a unique design that is faster and more flexible. In this paper, we design a new half adder and a new multiplier by nanotechnology using a ternary logic, which decreases the power consumption and chip surface and raises the speed. The presented design is simulated using CNTFET of Stanford University and HSPICE software, and the results are compared with those of other studies.     

Knowledge Discovery from Decision Tables by the Use of Multiple-Valued Logic

This paper describes how succinct rules, which reduce the size of decision tables, can be found by employing multiple-valued logic (MVL). Two multiple-valued algebras are described, one based on level detection, and the other on literal functions. Then a decision table which had also been reduced in size using rough set theory, is now reduced using both algebras and it is seen that all three approaches lead to reductions of comparable simplicity. The new methods require coding the values of each attribute as integers. Then an MVL function that maps the coding of the condition attributes to the coding of the decision attribute is found. As the coded table is sparse only some of the basis functions for each algebra are required. Then a simple approach requiring the reduction of a matrix to row echelon form is used to finding all suitable MVL functions. By decomposing a function in terms of its variables a complete set of rules can be found. The MVL function encodes the data in a very compact form and its decomposition into subfunctions reveals a good way to slice up the table into subtables. The structure of the subfunctions can then be used to simplify each subtable until compact sets of rules emerge. Alternatively, rules can be found by substitution into the MVL function. Encoding a decision table using MVL makes the data easy to manipulate and can uncover relationships that may not become apparent when using other methods.     

一种基于分离逻辑的块云存储系统验证工具

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.     

基于时序Petri网的联锁逻辑形式建模与验证

时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。     

Multi-Dimensional Modal Logic as a Framework for Spatio-Temporal Reasoning

In this paper we advocate the use of multi-dimensional modal logics as a framework for knowledge representation and, in particular, for representing spatio-temporal information. We construct a two-dimensional logic capable of describing topological relationships that change over time. This logic, called PSTL (Propositional Spatio-Temporal Logic) is the Cartesian product of the well-known temporal logic PTL and the modal logic S4_u, which is the Lewis system S4 augmented with the universal modality. Although it is an open problem whether the full PSTL is decidable, we show that it contains decidable fragments into which various temporal extensions (both point-based and interval based) of the spatial logic RCC-8 can be embedded. We consider known decidability and complexity results that are relevant to computation with multi-dimensional formalisms and discuss possible directions for further research.