首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到19条相似文献,搜索用时 203 毫秒
1.
郭亮  唐稚松 《软件学报》2003,14(1):54-61
使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.  相似文献   

2.
邓少波  黎敏  曹存根  眭跃飞 《软件学报》2015,26(9):2286-2296
提出具有模态词□φ=1V2φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,12是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=1V2φ;框架定义为三元组W,R1,R2,模型定义为四元组W,R1,R2,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果1的可达关系R1等于2的可达关系R2,那么该逻辑的公理化系统变成S5.  相似文献   

3.
Trace 演算   总被引:7,自引:4,他引:3  
黄涛  钱军  倪彬 《软件学报》1999,10(8):790-799
文章定义了基于踪迹(trace)的逻辑语言LTrace,它是一阶线性时序逻辑语言的扩充,同时也是“对象演算”研究工作的基础.Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体,语法上由对象标记表示.对象标记Ω=(S,F,A,E)包含4个部分:数据类型S、函数F、属性A和动作E.Σ=(S,F)构成通常代数规范意义下的标记,可将动作看成一广义数据类型,从而得到标记Σ的动作扩充ΣE.对象标记的语义解释结构由关于标记ΣE的代数、映射和动作与踪迹的关系定义.ΣE-代数给出关于数据参数的解释;映射给出属性在动作踪迹中所取的值;而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行.在定义了Trace演算的语法和语义之后,文章给出了Trace演算的公理系统及其可靠性证明.  相似文献   

4.
陶秋铭  赵琛  郭亮 《软件学报》2009,20(8):2074-2086
基于时序逻辑CTL(computation tree logic)的一种扩展CTL-FV对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画,采用含条件重写规则定义了保义语句交换Texch和保义变量替换Tsub,并基于一种归纳证明框架对它们的保义性进行了证明.此外,基于变换Texch对程序基本块内保依赖语句重排的保义性也给出了一种构造性的证明.  相似文献   

5.
独立多处理机任务静态调度问题的近似算法   总被引:1,自引:0,他引:1  
黄金贵  李荣珩 《软件学报》2010,21(12):3211-3219
研究独立多处理机任务静态调度问题Pm|fix|Cmax,即在m个处理机系统中调度n个多处理机任务,每个任务指派到所需一组处理机上不可剥夺地执行.该问题应用广泛但早已证明为NP难问题,而且也不存在常数近似算法.分析了问题Pm|fix|Cmax和其中所有任务都是单位处理机时间的特殊情形Pm|fix,p=1|Cmax的调度,并利用实例划分(split scheduling,简称SS)、首次满足优先(first fit,简称FF)和最大宽度优先(large wide first,简称LWF)等方法,构造了问题Pm|fix,p=1|Cmax的√2m +1近似算法和问题Pm|fix|Cmax的2√m 近似算法,优于目前已有文献的最好结果.  相似文献   

6.
k-LSAT (k≥3)是NP-完全的   总被引:1,自引:0,他引:1  
合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNFk是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSATk的NP-完全性取决于LCNFk是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF3和LCNF4中的不可满足公式,并提出公开问题:对于k≥5,LCNFk是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.  相似文献   

7.
相应于无冲突依赖的规范化对象模式森林   总被引:2,自引:1,他引:2  
吴永辉  周傲英 《软件学报》2002,13(8):1488-1493
首先概括对象依赖、无冲突对象依赖集合、规范化对象模式森林和复杂对象模式规范化设计算法的基本概念和性质;然后给出并证明相应于无冲突对象依赖集合M的规范化对象模式森林F的性质:P(F)是惟一的、不可分解的规范化对象模式森林的路径集合;M<=>OD(F)<=>P(F);P(F)是无(环的.这对于面向对象信息系统的开发有一定的意义.  相似文献   

8.
随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言(VASAML)与可验证应用系统体系结构建模方法(VASAMM).VASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t:T和Γ⊦RT1,T2)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程,包括构建Mbd(基本数据类型)、Mbti(基本接口类型)、Mdev(设备类型)和Mfrwk(应用系统框架)等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图(GDSI)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.  相似文献   

9.
给出矩阵方程 AX-EXY=BY的一个完全解析的、具有显式表达式和完全自由度的参数解 (X,Y) .这里假设矩阵束 (E,A,B) 为R-能控的, F为任意的方阵.相比于现有结论,求解算法不要求矩阵AF具有特殊的形式,且对它们的特征值没有任何的限制.此外,本文给出的通解还具有结构简洁的特点.作为一个应用,给出了广义系统正常Luenberger函数观测器的一种参数化的设计方法.算例证明了方法的有效性.  相似文献   

10.
金英  金成植 《软件学报》2003,14(1):16-22
Action演算簇(action calculi)作为描述不同并发交互行为的数学框架,可以表示一大类具有某些相同特性的并发形式化模型.试图把(演算(一种基于约束的高阶并发计算模)也包含在action演算簇的框架下.首先定义了一个具体的action演算AC(Kγ),然后给出了从(演算到AC(Kγ)转换的形式描述,最后在定义AC(Kγ)的可观察性、弱互模拟关系和弱等价关系的基础上,以(演算为中间表示,证明了这种转换保持了(演算的弱行为等价性.研究表明,action演算簇可以表示基于约束的并发模型,从而充分说明了action演算簇的描述能力,并且为在action演算簇框架下把(演算与其他并发模型结合并进行比较提供了前提.  相似文献   

11.
We study the problem of stabilization of nonlinear plants. We show that given a nonlinear plant P, if there exists a (nonlinear) compensator F, possibly unstable, which stabilizes P, then, with P1: = P(IF(− P))−1, any C defined by C:= F + Q(IP1Q)−1 for some finite-gain stable Q will stabilize P.  相似文献   

12.
Transformation of programs for fault-tolerance   总被引:2,自引:0,他引:2  
In this paper we describe how a program constructed for afault-free system can be transformed into afault-tolerant program for execution on a system which is susceptible to failures. A program is described by a set of atomic actions which perform transformations from states to states. We assume that a fault environment is represented by a programF. Interference by the fault environmentF on the execution of a programP can then be described as afault-transformation which transformsP into a program (P). This is proved to be equivalent to the programPP F , whereP F is derived fromP andF, and defines the union of the sets of actions ofP andF P . A recovery transformation transformsP into a program (P) =PR by adding a set ofrecovery actions R, called arecovery program. If the system isfailstop and faults do not affect recovery actions, we have ((P))=(P)R=PP F R We illustrate this approach to fault-tolerant programming by considering the problem of designing a protocol that guarantees reliable communication from a sender to a receiver in spite of faults in the communication channel between them.  相似文献   

13.
Let P(d) be a program implementing a partial recursive function φ. Let $ \mathcal{O} $ \mathcal{O} P denote a function defined on the domain of function φ that maps an input data d 0 onto the path of computation of P on the input d 0. Let Q(p, d) be a program returning a value if and only if p = $ \mathcal{O} $ \mathcal{O} P (d), and let the value of the program be Q($ \mathcal{O} $ \mathcal{O} P (d), d) = P(d). Program Q(p, d), which is totally absurd from the point of view of its practical computation on concrete input data, may be practically useful when it is analyzed by a metaprogram. It is shown in the paper how program Q(p, d) can be used for verification of a postcondition imposed on program P(d). The proposed method was tested on verification tasks for cache coherence protocols and other distributed computing systems.  相似文献   

14.
A grammar formF defines via a so-calledinterpretation mechanism, a family of languages(F). In this paper we establish that for many grammar formsF, (the family of context-free languages) implies(F)= RE (the family of recursively enumerable sets). We conjecture that this is also true in general. Because of this, it seems necessary to use restricted interpretations for non context-free grammar forms, a form giving then rise to a family We compare the obvious alternatives for restricting interpretations and focus attention on two promising alternatives, Q (F) and st(F) and their combination Q, st(F). Using st-interpretations, surprising families can be generated and strong normal form results can be obtained. Closure results and decidability results are also given. UnderQ, st-interpretation, it is possible to characterize a number of well-known families of languages between CF and RE, including the families of EOL, ETOL, matrix and scattered context languages.Part of this work was carried out while the third and fourth authors were visiting the University of Karlsruhe. Part of this work was supported by the Natural Sciences and Engineering Research Council of Canada Grant No. A-7700.  相似文献   

15.
Faults in a network may take various forms such as hardware failures while a node or a link stops functioning, software errors, or even missing of transmitted packets. In this paper, we study the link-fault-tolerant capability of an n-dimensional hypercube (n-cube for short) with respect to path embedding of variable lengths in the range from the shortest to the longest. Let F be a set consisting of faulty links in a wounded n-cube Qn, in which every node is still incident to at least two fault-free links. Then we show that Qn-F has a path of any odd (resp. even) length in the range from the distance to 2n-1 (resp. 2n-2) between two arbitrary nodes even if |F|=2n-5. In order to tackle this problem, we also investigate the fault diameter of an n-cube with hybrid node and link faults.  相似文献   

16.
A Hamiltonian path in G is a path which contains every vertex of G exactly once. Two Hamiltonian paths P 1=〈u 1,u 2,…,u n 〉 and P 2=〈v 1,v 2,…,v n 〉 of G are said to be independent if u 1=v 1, u n =v n , and u i v i for all 1<i<n; and both are full-independent if u i v i for all 1≤in. Moreover, P 1 and P 2 are independent starting at u 1, if u 1=v 1 and u i v i for all 1<in. A set of Hamiltonian paths {P 1,P 2,…,P k } of G are pairwise independent (respectively, pairwise full-independent, pairwise independent starting at u 1) if any two different Hamiltonian paths in the set are independent (respectively, full-independent, independent starting at u 1). A bipartite graph G is Hamiltonian-laceable if there exists a Hamiltonian path between any two vertices from different partite sets. It is well known that an n-dimensional hypercube Q n is bipartite with two partite sets of equal size. Let F be the set of faulty edges of Q n . In this paper, we show the following results:
1.  When |F|≤n−4, Q n F−{x,y} remains Hamiltonian-laceable, where x and y are any two vertices from different partite sets and n≥4.
2.  When |F|≤n−2, Q n F contains (n−|F|−1)-pairwise full-independent Hamiltonian paths between n−|F|−1 pairs of adjacent vertices, where n≥2.
3.  When |F|≤n−2, Q n F contains (n−|F|−1)-pairwise independent Hamiltonian paths starting at any vertex v in a partite set to n−|F|−1 distinct vertices in the other partite set, where n≥2.
4.  When 1≤|F|≤n−2, Q n F contains (n−|F|−1)-pairwise independent Hamiltonian paths between any two vertices from different partite sets, where n≥3.
  相似文献   

17.
This paper studies H fault-tolerant control for a class of uncertain nonlinear systems subject to time-varied actuator faults. A radial basis function neural network is utilised to approximate the unknown nonlinear functions; an updating rule is designed to estimate on-line time-varied fault of actuator; and the controller with the states feedback and faults estimation is applied to compensate for the effects of fault and minimise H performance criteria in order to get a desired H disturbance rejection constraint. Sufficient conditions are derived, which guarantees that the closed-loop system is robustly stable and satisfies the H performance in both normal and fault cases. In order to reduce computing cost, a simplified algorithm of matrix Riccati inequality is given. A spacecraft model is presented to demonstrate the effectiveness of the proposed methods.  相似文献   

18.
Tools for computational differentiation transform a program that computes a numerical function F(x) into a related program that computes F(x) (the derivative of F). This paper describes how techniques similar to those used in computational-differentiation tools can be used to implement other program transformations—in particular, a variety of transformations for computational divided differencing. The specific technical contributions of the paper are as follows:– It presents a program transformation that, given a numerical function F(x) defined by a program, creates a program that computes F[x 0, x 1], the first divided difference of F(x), where – It shows how computational first divided differencing generalizes computational differentiation.– It presents a second program transformation that permits the creation of higher-order divided differences of a numerical function defined by a program.– It shows how to extend these techniques to handle functions of several variables.The paper also discusses how computational divided-differencing techniques could lead to faster and/or more robust programs in scientific and graphics applications.Finally, the paper describes how computational divided differencing relates to the numerical-finite-differencing techniques that motivated Robert Paige's work on finite differencing of set-valued expressions in SETL programs.  相似文献   

19.
计算机系统的容错技术方法   总被引:1,自引:0,他引:1  
随着计算机技术的发展,计算机系统的可靠性越来越受到人们的重视,而容错技术是提高可靠性的一种有效方法。本文研究了计算机容错技术的各种方法,如硬件容错、信息容错、软件容错等,介绍了TMR(三模冗余)的原理及其缺点,详细研究了两种最基本的软件容错技术NVP和RB。这些容错技术可有效提高计算机系统的可靠性。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号