When is `partial' adequate? A logic-based proof technique using partial specifications

A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples

卫星激光通信Ⅱ地面检测和验证技术

星间激光通信终端的主要技术指标和运行性能必须事先在地面实验室条件下进行模拟检验, 因此在研制卫星激光通信终端的同时必须发展相应的系统性检测和验证平台, 主要包括激光通信性能检验、光跟瞄性能检验和光束质量检验。本文综述了卫星激光通信终端检验技术的国外进展, 介绍了我们全物理模拟的地面检测验证思路和方法。

全固态激光技术在航天领域的应用

回顾了空间固体激光应用系统的发展，以激光雷达和激光测高仪为主．介绍了国外几种典型应用系统的性能、指标及其全固态激光发射器的关键技术。最后介绍了我国探月工程中激光测高仪的研制情况。

Design and properties analysis of multi-layer dielectric used in pulse compressor gratings

Used in chirped-pulse amplification system and based on multi-layer thin film stack, pulse compressor gratings (PCG) are etched by ion-beam and holographic techniques. Diffraction efficiency and laser-induced damage threshold rely on the structural parameters of gratings. On the other hand, they depend greatly on the design of multi-layer. A theoretic design is given for dielectric multi-layer, which is exposed at 413.1 nm and used at 1053 nm. The influences of coating design on optical characters are described in detail. The analysis shows that a coating stack of H3L (H2L) (boolean AND) 9H0.5L2.01H meets the specifications of PCG well. And there is good agreement of transmission between experimental and the theoretic design. (c) 2005 Elsevier GmbH. All rights reserved.

Tunneling transmission in two quantum wires coupled by a magnetically defined barrier

A numerical analysis of an electron waveguide coupler based on two quantum wires coupled by a magnetically defined barrier is presented with the use of the scattering-matrix method. For different geometry parameters and magnetic fields, tunneling transmission spectrum is obtained as a function of the electron energy. Different from that of conventional electron waveguide couplers, the transmission spectrum of the magnetically coupled quantum wires does not have the symmetry with regard to those geometrically symmetrical ports, It was found that the magnetic field in the coupling region drastically enhances the coupling between the two quantum wires for one specific input port while it weakens the coupling for the other input port. The results can be well understood by the formation of the edge states in the magnetically defined barrier region. Thus, whether these edge states couple or decouple to the electronic propagation modes in the two quantum wires, strongly depend on the relative moving directions of electrons in the propagating mode in the input port and the edge states in the magnetic region. This leads to a big difference in transmission coefficients between two quantum wires when injecting electrons via different input ports. Two important coupler specifications, the directivity and uniformity, are calculated which show that the system we considered behaves as a good quantum directional coupler. (C) 1997 American Institute of Physics.

Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

The Category-Theoretic Solution of Recursive Domain Equations

Recursive specifications of domains plays a crucial role in denotational semantics as developed by Scott and Strachey and their followers. The purpose of the present paper is to set up a categorical framework in which the known techniques for solving these equations find a natural place. The idea is to follow the well-known analogy between partial orders and categories, generalizing from least fixed-points of continuous functions over cpos to initial ones of continuous functors over $\omega $-categories. To apply these general ideas we introduce Wand's ${\bf O}$-categories where the morphism-sets have a partial order structure and which include almost all the categories occurring in semantics. The idea is to find solutions in a derived category of embeddings and we give order-theoretic conditions which are easy to verify and which imply the needed categorical ones. The main tool is a very general form of the limit-colimit coincidence remarked by Scott. In the concluding section we outline how compatibility considerations are to be included in the framework. A future paper will show how Scott's universal domain method can be included too.

function definition language fdl and its implementation

A Function Definition Language (FDL) is presented. Though designed for describing specifications, FDL is also a general-purpose functional programming language. It uses context-free language as data type, supports pattern matching definition of functions, offers several function definition forms, and is executable. It is shown that FDL has strong expressiveness, is easy to use and describes algorithms concisely and naturally. An interpreter of FDL is introduced. Experiments and discussion are included.

facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.

basic research in computer science and software engineering at sklcs

The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.

基于CTL的循环优化变换描述方法

TRANS是基于CTL的优化变换描述语言,对TRANS语言作了宏扩展,给出了循环嵌套、循环归纳变量、循环依赖及方向向量的时序逻辑描述.从依赖分析的角度对重排序循环优化变换加以考查,并以循环逆转和循环交换为例阐述了其形式化描述方法.

多媒体节目时序描述的完全性和协调性

完全性和协调性是形式规范的两个基本性质 .针对不同的形式规范 ,完全性和协调性的定义可能是不同的 .该文首先根据通信顺序进程的理论 ,把一个多媒体流用两个瞬时事件表示 ,并且定义了时间区间向量的概念和在它之上的一些运算 .基于这些准备工作 ,文中给出了多媒体系统中媒体对象时序关系描述的完全性和协调性的形式定义 .由于文中讨论的时序描述语言较简单 ,但是对于多媒体领域又是足够的 ,因此 ,与相关工作比较 ,该文研究的完全性和协调性的形式定义更直观 ,判定算法也更高效

基于形式描述的编译优化自动测试方法与技术研究

编译优化是现代编译器不可缺少的重要功能。编译优化技术在过去几十年里取得了显著进展，对提升程序运行速度、节省存储空间、节省能耗等起到了不可替代的作用。然而，编译优化的可靠性却不尽人意。编译优化技术种类多、处理复杂而且可复用性弱，容易出错，即便是成熟的编译器，也不断有与编译优化相关的bug被发现出来。编译器的可靠性对软件产品的可靠性和安全性有直接影响，随着编译优化在现代编译器中的比重不断增加，编译优化的可靠性也日益受到人们的关注。 软件测试是保障编译优化可靠性的基本技术手段之一，然而，编译优化测试涉及测试程序编写、测试执行等过程，人工完成相当费时费力，因此有必要研究编译优化自动测试方法，以提高编译优化测试的效率。基于这一实际需求，Intel、MEI (Matsushita Electric Industrial)、DaimlerChrysler AG等业界产商近年来也相继与有关研究机构开展合作，研究编译优化自动测试方法。 目前已有的编译器自动测试方法中大多数都是以程序设计语言的语法和语义为主要依据，适用于测试语法检查、语义检查、代码生成等基本编译功能，对于编译优化的测试则缺乏针对性，测试效率较低，而已有的若干种面向编译优化的自动测试方法也存在着对编译优化刻画不够准确、自动化程度不高等缺陷。 本文提出一种基于形式描述的编译优化自动测试方法(TEMCOFS)，其实现过程分为四个阶段，即：(1) 建立编译优化形式描述；(2) 分析编译优化描述的正确性；(3) 基于编译优化形式描述自动生成测试程序；(4) 自动执行测试。在TEMCOFS方法框架下，本文分别研究了编译优化形式化描述方法、编译优化描述正确性分析方法和基于形式描述的两种自动测试方法，实现了三类典型优化—表达式优化、数据流优化、循环优化的自动测试，主要工作包括： (1) 在编译优化形式描述方面，除了应用前人研究成果—TRANS语言描述了表达式优化和数据流优化之外，还对TRANS语言进行了扩展，建立了循环优化的形式描述机制； (2) 在编译优化正确性分析方面，首先证明了揭示程序数据依赖关系对程序变换正确性影响的依赖基础定理，为循环优化正确性分析提供了基础，然后探讨了编译优化正确性分析的一般方法； (3) 在测试自动执行方面，提出了编译优化自动变形测试执行方法，该方法将变形测试思想引入编译优化测试中，利用测试程序等价性质实现测试结果的自动判定，能够避免传统方法中测试结果判定所存在的问题； (4) 在测试程序自动生成方面，分别对应两种测试自动执行方法—比照法和变形法提出了基于编译优化形式描述的测试程序自动生成方法，能够根据表达式优化、数据流优化、循环优化的形式描述自动生成测试程序集。 在GCC编译器上的实验表明，基于本文方法自动生成的测试程序集可使GCC的编译优化模块较快达到较高的测试覆盖率。与其他编译器自动测试方法相比，本文方法对编译优化测试的针对性较好，自动化程度也较高。总而言之，本文方法对于提高编译优化测试效率、保障优化编译器的质量具有较好的实用和参考价值。

一类基于IPO的工作流过程建模语言规范分析

在工作流管理系统中,过程模型信息的交换是通过过程建模语言来实现的。不同的过程模型由其专有语言来定义,它们的表达方式可作为选择建模语言的基准。该文首先介绍现已存在的工作流过程建模语言的分类,然后针对其中的一类,着重对两个比较典型的过程定义语言规范进行了分析和比较。