并发进程系统正确性的验证图式

并发进程系统正确性的验证,比之顺序进程正确性的验证有其特殊意义。并发系统的运行,在执行序列这一级上是非决定的,通常的调试手段,很难暴露系统中依赖于执行序列的那类错误。因此并发系统正确性的验证,在三种不同水平上都是有价值的:完全形式化的形式演绎系统;半形式化的数学证明;或者有效的检查调试方法。 并发系统运行的非决定性,也极大地增加了验证的复杂性。在证明系统具有某个性质时,粗略地说,就是要证明这个系统的所有执行序列都具有这种性质。一个顺序进程,从给定的初始状态出发,只有一个可能的执行序列;但是多个并发进程的可能执行序列则往往是无穷多个。由于这种复杂性禁锢了人们的智力活动,使得一些简单的事实,人们也很难将其严格证明。系统中存在的问题,事后看来即使是一些很明显的问题,也会被这种复杂性掩盖起来,长时间不被发现。     

命题演算形式系统在Isabelle／HOL中的形式化

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle／HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明。通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。     

基于优先执行关系闭包运算的事务可串行化判定方法

现代数据库技术支持并发用户,会产生大量的并发事务。为了提高数据库系统的性能和维护系统的一致性,必须保证事务并发执行的可串行化调度。可串行化检测是数据库系统中事务管理的关键技术,一般采用执行图的判定方法。从关系运算的代数方法出发,提出基于事务执行优先关系的闭包运算和由此建立的联合逻辑公式的计算,通过逻辑判定来检验并发事务的可串行化。通过定理证明和实例验证,该方法取得了同执行图判定相同的效果,而且判定更直观,更易于操作实现,不需要建立复杂的图数据结构和在图搜索中检测环是否出现。     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

相干命题逻辑自然推理系统NR的自动证明*

给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理。     

基于CPN对系统的并发行为进行测试

首先对基本并发行为进行CPN建模及状态空间生成,逐渐增大模型的复杂性,展示了CPN建模并发行为可能存在的状态空间快速增大问题。在保证并发覆盖的前提下,将测试序列的生成划分为3个阶段,重点讨论了覆盖并发行为的测试序列生成方法。对于并发开始(末)库所按照CPN执行产生的状态空间中的节点进行了映射,得到状态空间中对应并发的开始(末)库所的开始(末)节点集合。通过对并发的开始(末)节点集内的节点间的关系进行分析,依据它们在状态空间中的前驱后继关系 ,生成一个由开始(末)节点的序列构成的序列的集合,然后以此序列集内的序列作为覆盖并发行为的测试序列的开始部分或者结尾部分,生成覆盖并发的测试序列。通过一个自行实现的P2P软件,使用了提出的建模方法及测试序列生成算法。最后通过得到的测试序列设计了测试场景及测试方案,包括Tracker并发行为测试系统结构、服务器测试方案及典型的测试场景设计。将P2P软件和TTCN-3测试机部署在一起实现了TTCN-3测试套的执行,测试结果表明测试工作的设计与实现是正确的。     

实时系统时间并行模型确定性分析

研究实时并行系统的确定性,采用面向执行体构件建模和广义测度固定点理论研究系统收敛条件.把实时系统构建为用时间信号联系的面向执行的构件集合,采用超致密时间(SDT)表示混合系统信号标签模型,定义构件为时间模型上的偏序集函数,构成有反馈作用的偏序集函数组合,用广义超测度空间固定点理论分析时间并行模型因果构件的收敛性和系统响应的存在和唯一性.     

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.     

用代数系统描述数据对象及其操作方法的研究

本文旨在研究使用代数系统对CMM管理工具所需数据对象及其上操作进行统一描述的方法，结合代数系统的定义和定理，将数据对象的全体看作集合，将数据对象上的各种操作定义成该集合上的运算，从而构成代数系统，实例证明,本方法可以和已有的抽象代数系统联系起来，从而为控制数据对象上的各种操作提供可靠的理论依据。     

On the determinacy of concurrent games on event structures with infinite winning sets

We consider nondeterministic concurrent games played on event structures and study their determinacy problem—the existence of winning strategies. It is known that when the winning conditions of the games are characterised by a collection of finite winning sets/plays, a restriction (called race-freedom) on the boards where the games are played guarantees determinacy. However the games may no longer be determined when the winning sets are infinite. This paper provides a study of concurrent games and nondeterministic winning strategies by analysing conditions that ensure determinacy when infinitely many events are played, that is, when the winning sets are infinite. The main result is a determinacy theorem for a class of games with a bounded concurrency property and infinite winning sets shown to be finitely decidable.     

变精度粗糙集推广模型及其性质研究

数据挖掘的主要目标之一是进行有效分类,粗糙集的上下近似空间正是为了对信息系统进行分类。变精度粗糙集作为经典粗糙集的推广模型,目前研究仅局限于有限集。针对变精度粗糙集模型无法处理无限集合的问题,在变精度粗糙集和测度的理论基础上,提出了基于Lebesgue测度的变精度粗糙集模型。首先,引入Lebesgue测度的概念,构造了一种基于Lebesgue测度的变精度粗糙集模型,将变精度粗糙集理论推广到无限集;其次,定义了该模型的上、下近似空间;最后,证明了其相关性质。通过理论研究表明,该模型能有效处理无限集合问题,对变精度粗糙集的理论研究形成突破,也将极大的扩充其应用范围。     

An information theoretic approach to dynamical systems modeling and identification

The identification and modeling of dynamical systems in a practical situation, where the model set under consideration does not necessarily include the observed system, are treated. A measure of the relevant information in a sequence of observations is shown to possess useful properties, such as the metric property on the parameter set. It is then shown that maximum likelihood and related Bayesian identification procedures converge to a model in the model set, which is closest to the actual system generating the observations in the information distance measure. The convergence analysis is restricted for simplicity to finite sets of models. The analysis naturally suggests methods for approximating a high-order system by a low-order model and for selecting a representative model from a given model set, applicable to infinite and even noncompact model sets.     

Closed schedulers: a novel technique for analyzing asynchronous protocols

Summary Analyzing distributed protocols in various models often involves a careful analysis of the set ofadmissible runs, for which the protocols should behave correctly. In particular, the admissible runs assumed by at-resilient protocol are runs which are fair for all but at mostt processors. In this paper we defineclosed sets of runs, and suggest a technique to prove impossibility results fort-resilient protocols, by restricting the corresponding sets of admissible runs to smaller sets, which are closed, as follows: For each protocolPR and for each initial configurationc, the set of admissible runs ofPR which start fromc defines a tree in a natural way: the root of the tree is the empty run, and each vertex in it denotes a finite prefix of an admissible run; a vertexu in the tree has a sonv iffv is also a prefix of an admissible run, which extendsu by one atomic step.The tree of admissible runs described above may contain infinite paths which are not admissible runs. A set of admissible runs isclosed if for every possible initial configurationc, each path in the tree of admissible runs starting fromc is also an admissible run. Closed sets of runs have the simple combinatorial structure of the set of paths of an infinite tree, which makes them easier to analyze. We introduce a unified method for constructing closed sets of admissible runs by using a model-independent construction of closedschedulers, and then mapping these schedulers to closed sets of runs. We use this construction to provide a unified proof of impossibility of consensus protocols. Ronit Lubitch received her B.Sc. degree in Mathematics and Computer Science from Tel Aviv University in 1989, and her Master degree in Computer Science from the Technion, in 1993. From 1992 she is working in Graffiti Software Industries, which expertise in the design and development of advanced photo realistic rendering, and animation software systems. Shlomo Moran received his B.Sc. and Ph.D. degrees in Mathematics from the Technion in 1975 and 1979 resp. In 1979–1981 he was at the University of Minnesota as a visiting research specialist. In 1981 he joined the Computer Science Department at the Technion, where he is now a full professor. In 1985–1986 he visited at IBM T.J. Watson Research Center. In 1992–1993 he visited at AT&T Bell Laboratories and in Centrum voor Wiskunde en Informatica, Amsterdam. His research interests include distributed computing, Combinatorics and Graph Theory, and Complexity Theory.A preliminary extended version of this paper appeared in the Proceedings of 6-th International Workshop on Distributed Algorithms, Haifa, November 1992This work was supported in part by the Technion V.P.R. fund. Part of this research was conducted while this author was visiting at AT&T Bell Labs at Murray Hill and at CWI, Amsterdam     

Model checking for process rewrite systems and a class of action-based regular properties

We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL.     

基于ASP的CSP并发系统验证研究

传统并发通信顺序进程(CSP>性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证 工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验 证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转 换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系 统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。     

LQR and LQG based optimal switching techniques for PSS and UPFC in power systems

Selection of better optimized unified power flow controller (UPFC) control inputs along with simultaneous coordinated design of power system stabilizer (PSS) is a challenge in the present scenario of power systems. Hence, in this paper, four sets of experiments performed are presented. First set of experiments are without disturbance scenario where switching is done using linear quadratic regulators (LQR’s). Second set is for power systems with disturbances using linear quadratic gaussian (LQG). Switching control algorithms presented here are tested on the single machine infinite bus (SMIB) linearised Phillips Heffron model of power system using MATLAB/SIMULINKr platform.     

A Fully Abstract Semantics for Concurrent Constraint Programming

A compositional and fully abstract semantics for concurrent constraint programming is developed. It is the first fully abstract semantics which takes into account both non-determinism, infinite computations, and fairness. We present a simple concurrent constraint programming language, whose semantics is given by a set of reduction rules augmented with fairness requirements. In the fully abstract semantics we consider two aspects of a trace, viz. the function computed by the trace (the functionality) and the set of input and output data (the limit of the trace). We then derive the fully abstract semantics from the set of traces using a closure operation. We give two proofs of full abstraction; the first relies on the use of a syntactically infinite context. The second proof requires only a finite context, but assumes as input a representation of the function to be computed by the context. Finally, we examine the algebraic properties of the programming language with respect to the fully abstract semantics. It turns out that the non-deterministic selection operation can be defined using operations derived from parallel composition and the usual set-theoretic operations on sets of traces.     

Parallel generation of infinite images

We introduce a syntactic model for generating sets of finite and infinite images where a finite image can be viewed as an array over finite alphabet and an infinite image is an array with finite number of columns and infinite number of rows. This model, called image grammar, can be considered as a generalization of classical Chromsky grammar.

We study various types of infinite image grammars using Nivat's derivation which is an infinite unrestrictive derivation, Bvichi's (respectively Muller's) which is defined as infinite derivations selected by some repetitive set (respectively sets of rewriting rules). Then we study the combinatorial and language theoretical properties such as complexity measure, closure properties and decidability results. In terms of complexity measure we give a strict infinite hierarchy. We have extended Nivat's and Eilenberg's theorems to infinite images. Unfortunately we prove that Biichi's and McNaughton's theorems cannot be extended to infinite images. We also characterize these families in terms of deterministic image co-substitution and ω-languages     

A note on the Hartley-like measure of uncertainty

The principal aim of this paper is to bring the relatively little-known Hartley-like measure of uncertainty to the attention of readers of this journal. First, the reader is introduced to the classical Hartley measure of uncertainty, applicable to finite sets, and to the complementary Hartley-like measure of uncertainty, applicable to infinite sets. This is followed by an overview of some well-known applications of these measures to classical sets as well as standard fuzzy sets of possible alternatives. Applications of the Hartley-like measure to two types of non-standard fuzzy sets are then explored. This paper concludes with a discussion of two open research problems regarding the Hartley-like measure, solutions of which are essential for overcoming some practical limitations of this measure.