基于时态逻辑的协议RSL形式化描述

研究以RAISE规范语言(RSL)描述时态逻辑中always算子、sometimes算子和until算子的方法以及对复合时态算子的描述方法,提出在时态逻辑模型基础上用RSL对协议进行形式化描述的步骤,以AB协议为示例,给出其基于时态逻辑模型的RSL描述,从而证明该描述模型有利于协议验证和协议测试用例生成的自动实现。     

The programming language standards scene, ten years on Paper 15: Vienna Development Method Specification Language (VDM-SL)

This paper, one of a simultaneously published set, describes the establishment in 1987 of the ISO standards project for the Vienna Development Method Specification Language (VDM-SL), and the progress of the project to the end of 1993.     

A functional νMOS circuit for implementing cellular-automaton picture-processing devices

This paper proposes a design of cell circuits for implementing cellular-automaton devices that perform morphological picture processing. To produce the complex cell functions required for the morphological processing, we present the idea of using the silicon functional device, ν-MOS FET. We designed sample cell circuits for several morphological processings, and simulated their operation to show the expected cell operation. We also designed a sample cellular-automaton circuit using the proposed cell circuits, and demonstrated in simulation its example processing (noise cleaning and edge extraction in an image). A low dissipation of about 20 μW per cell circuit can be expected at 1 MHz operation; therefore, 10⁵ or more cells that operate in parallel can be integrated into an LSI.     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

Graphical Verification of a Spatial Logic for the π-calculus

The paper introduces a novel approach to the verification of spatial properties for finite π-calculus specifications. The mechanism is based on a recently proposed graphical encoding for mobile calculi: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Spatial properties for reasoning about the behavior and the structure of π-calculus processes are then expressed in a logic introduced by Caires, and they are verified on the graphical encoding of a process, rather than on its textual representation. More precisely, the graphical presentation allows for providing a simple and easy to implement verification algorithm based on the graphical encoding (returning true if and only if a given process verifies a given spatial formula).