Eliminating the substitution axiom from UNITY logic

The UNITY substitution axiom, if (x=y) is an invariant of a program, then x can be replaced by y in any property of the program, is problematic for several reasons. In this paper, dual predicate transformerssst andwst are introduced that allow the strongest invariant of a program to be expressed, and these are used to give new definitions for the temporal operatorsunless andensures. With the new definitions, the substitutionaxiom is no longer needed, and can be replaced by a derived rule of inference which is formally justified in the logic. One important advantage is that the effects of the initial conditions on the properties of a program are formally captured in a convenient way, and one can forget about substitution in formal treatments of the UNITY proof system while still having it available when desirable to use during the derivation of programs. Composibility and completeness of the modified logic are also discussed.     

A Notation and Logic for Mobile Computing

We define a concurrent mobile system as one where independently executing components may migrate through some space during the course of the computation, and where the pattern of connectivity among the components changes as they move in and out of proximity. The definition is general enough to encompass a system of mobile hosts moving in physical space as well as a system of migrating software agents implemented on a set of possibly non-mobile hosts. In this paper, we present Mobile UNITY, a notation for expressing mobile computations and a logic for reasoning about their temporal properties. Our goal is to find a minimalist model of mobile computation that will allow us to express mobile components in a modular fashion and to reason formally about the possible behaviors of a system composed from mobile components. A simplified serial communication protocol among components which can move in space serves as an illustration for the notation.     

Modeling adaptive behaviors in Context UNITY

Context-aware computing refers to a paradigm in which applications sense aspects of the environment and use this information to adjust their behavior in response to changing circumstances. In this paper, we present a formal model and notation (Context UNITY) for expressing quintessential aspects of context-aware computations; existential quantification, for instance, proves to be highly effective in capturing the notion of discovery in open systems. Furthermore, Context UNITY treats context in a manner that is relative to the specific needs of an individual application and promotes an approach to context maintenance that is transparent to the application. In this paper, we construct the model from first principles, introduce its proof logic, and demonstrate how the model can be used as an effective abstraction tool for context-aware applications and middleware.     

并行软件功能规约的组合语义方法

文章提出了一种将代数语义、Hoars逻辑和UNITY逻辑集成在一起描述并行软件功能规约的方法。其目的在于充分发挥并集成代数语义描述抽象数据类型、Hoars逻辑描述功能、UNITY逻辑描述并行程序性质的优点。表示形式有利于规约的分解、细化和验证。     

UNITY与典型程序设计模型的比较

UNITY是一种简单统一的理论、计算模型和证明系统,而且具有很强的把UNITY程序映射成不同的计算机体系结构模式的能力。该文在简述UNITY机理的基础上,分析UNITY与几种典型的程序设计模型(函数式、命令式、逻辑式、基于规则式、Petri网、CSP)的区别,并给出它们对应的等价UNITY程序转换,最后,介绍Seuss对完善UNITY的新策略。     

Data refinement of mixed specifications

Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY style specifications to be written as a combination of abstract program and temporal properties. From the point of view of the programmer, mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized ‘always section’. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example. Received: 1 April 1996 / 6 March 1997     

Mapping PUNITY to UniNet

To solve the problems of the interleaving assumption and the single resource in PUNITY(Petri net and UNITY) and Petri net respectively,this paper proposes a set of mapping rules from PUNITY to uniNet.Based on these rules,problems of one field can be transformed to problems of the other field and powerful tools of Petri net and UNITY can be used.The paper gives a sketch of the mapping rules and applies the rules to an example.Meanwhile ,the mapping rules can help computer to translate PUNITY to UniNet easily.     

A UNITY-style programming logic for shared dataspace programs

A proof system for a shared dataspace programming notation called Swarm (a programming logic similar in style to that of UNITY) is specified. Relevant aspects of the Swarm language and model are overviewed. To illustrate the proof system, the Swarm logic is used to verify the correctness of a program for labeling connected equal-intensity regions of a digital image. Like UNITY, the Swarm proof system uses an assertional programming logic which relies upon proof of programwide properties, e.g. global invariants and progress properties. The Swarm logic is defined in terms of the same logical relations as UNITY (unless, ensures, and leads-to), but several of the concepts are reformulated to accommodate Swarm's distinctive features     

Mechanizing compositional reasoning for concurrent systems: some lessons

The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The proposals investigated include existential/universal properties, guarantees properties and progress sets. The results also apply to related proposals such as traditional assumption-commitment guarantees and Misras closure properties. Findings that have been published in detail elsewhere are summarised and consolidated here. One conclusion is that UNITY and related formalisms leave some important issues implicit, such as their concept of the program state, which means that great care must be exercised when implementing tool support. Another conclusion is that many compositional reasoning methods can be mechanized, provided that the issues mentioned above are correctly addressed.Received November 2003Revised November 2004Accepted November 2004 by C. B. Jones     

Compositional programming abstractions for mobile computing

Recent advances in wireless networking technology and the increasing demand for ubiquitous, mobile connectivity demonstrate the importance of providing reliable systems for managing the reconfiguration and disconnection of components. The design of such systems requires tools and techniques appropriate to the task. Many formal models of computation, including UNITY, are not adequate for expressing reconfiguration and disconnection and are, therefore, inappropriate vehicles for investigating the impact of mobility on the construction of modular and composable systems. Algebraic formalisms such as the π-calculus have been proposed for modeling mobility. This paper addresses the question of whether UNITY, a state-based formalism with a foundation in temporal logic, can be extended to address concurrent, mobile systems. In the process, we examine some new abstractions for communication among mobile components that express reconfiguration and disconnection and which can be composed in a modular fashion     

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向.为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统.在此基础上严格的证明了TIA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件.最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型.     

Formal verification of concurrent programs using the Larch prover

The paper describes the use of the Larch prover to verify concurrent programs. The chosen specification environment is UNITY, whose proposed model can be fruitfully applied to a wide variety of problems and modified or extended for special purposes. Moreover, UNITY provides a high level of abstraction to express solutions to parallel programming problems. We investigate how the UNITY methodology can be mechanized within a general purpose first order logic theorem prover like LP, and how we can use the theorem proving methodology to prove safety and liveness properties. Then we describe the formalization and the verification of a communication protocol over faulty channels, using the Larch prover LP. We present the full computer checked proof, and we show that a theorem prover can be used to detect flaws in a system specification     

CODEWEAVE: Exploring Fine-Grained Mobility of Code

This paper is concerned with an abstract exploration of code mobility constructs designed for use in settings where the level of granularity associated with the mobile units exhibits significant variability. Units of mobility that are both finer and coarser grained than the unit of execution are examined. To accomplish this, we take the extreme view that every line of code and every variable declaration are potentially mobile, i.e., it may be duplicated or moved from one program context to another on the same host or across the network. We also assume that complex code assemblies may move with equal ease. The result is CODEWEAVE, a model that shows how to develop new forms of code mobility, assign them precise meaning, and facilitate formal verification of programs employing them. The design of CODEWEAVE relies greatly on Mobile UNITY, a notation and proof logic for mobile computing. Mobile UNITY offers a computational milieu for examining a wide range of constructs and semantic alternatives in a clean abstract setting, i.e., unconstrained by compilation and performance considerations traditionally associated with programming language design. Ultimately, the notation offered by CODEWEAVE is given exact semantic definition by means of a direct mapping to the underlying Mobile UNITY model. The abstract and formal treatment of code mobility offered by CODEWEAVE establishes a technical foundation for examining competing proposals and for subsequent integration of some of the mobility constructs both at the language level and within middleware for mobility.     

行为时序逻辑与自反线性时序逻辑的关系

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。     

扩展时段时序逻辑的模型、一致性和推理

给出了扩展时段时序逻辑的时间Petri网（TPN）模型构造方法，在构造模型的同时对时序关系进行一致性检验，在模型的基础上提出了一种时序关系推理算法，这种推理算法基于TPN模型的性质及基本不等式规则，可由一组已知的扩展时段时序关系推出一些未知的扩展时段时序关系，这种推广理算法的优势在于利用了TNP模型的分析技术，减小了推理的时间复杂度比单纯利用不等式规则的推理更直观，也更简单，是一种有效的方法，最后，对扩展时段时序逻辑的TPN模型进行了扩充，增强了其模型和分析的能力。     

淋巴细胞的时间语义逻辑模型及其演化策略

数字序列抗原内部存在许多语义特征,针对抗原进行语义识别可以提高系统检测的准确性。基于抗原的相对时序关系,该文采用了一阶逻辑作为抗原和淋巴细胞的基本描述语言,以扩展逻辑程序构造淋巴细胞的时间语义逻辑模型,给出了淋巴细胞的逻辑表示形式。基于逻辑程序的稳定模型语义学,用稳定模型语义计算作为新的淋巴细胞的匹配算法。借鉴遗传归纳逻辑程序GILP的基本思想,给出了新的淋巴细胞的演化算法。     

Cut-free sequent systems for temporal logic

Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.     

Streamlining progress-based derivations of concurrent programs

The logic of Owicki and Gries is a well-known logic for verifying safety properties of concurrent programs. Using this logic, Feijen and van Gasteren describe a method for deriving concurrent programs based on safety. In this work, we explore derivation techniques of concurrent programs using progress-based reasoning. We use a framework that combines the safety logic of Owicki and Gries, and the progress logic of UNITY. Our contributions improve the applicability of our earlier techniques by reducing the calculational overhead in the formal proofs and derivations. To demonstrate the effectiveness of our techniques, a derivation of Dekker’s mutual exclusion algorithm is presented. This derivation leads to the discovery of some new and simpler variants of this famous algorithm. Author Mooij performed this research at the Department of Mathematics and Computer Science of the Technische Universiteit Eindhoven, while being supported by the NWO under project 016.023.015: “Improving the Quality of Protocol Standards”. E. C. R. Hehner