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的工作流过程建模语言规范分析

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

A novel quantum directional coupler based on Pi-shaped coupled electron waveguides

We explore the possibility of a quantum directional coupler based on Pi-shaped coupled electron waveguides with smooth boundaries. By calculating the transmission spectra, we propose an optimized coupler structure with a high directivity and fine uniformity. The coupler specifications, directivity, uniformity, and coupling coefficient are evaluated.

机器人研磨抛光工艺研究与实现

机器人研磨抛光工艺研究建立在大量机器人磨抛试验的基础上。本文针对加工对象——有机玻璃,在满足被加工工件质量的前提下,确定了机器人研磨抛光加工时磨片的合理使用顺序、规划加工路径和安排正交试验,以获得机器人磨抛加工的最优工艺参数组合,并制定机器人磨抛的加工策略。最后通过机器人研磨抛光加工实例,进一步验证了机器人的研磨抛光工艺知识有其合理性。

PXJ-Ⅱ排险机器人

介绍了一种可在危险环境下作业的遥控机器人──PXJ－Ⅱ排险机器人，分析了其功能指标及结构，简述了以武器系统和传感器为主的机器人辅助系统及其实用意义。

多关节机器人工作空间的分析与评价方法

本文运用 H-D 变换的基本原理,结合极坐标变换导出了产生n自由度多关节机器人工作空间的递推算法,当给定了机器人的结构尺寸,即可将机器人工作空间在一特定平面内的边界图形用计算机打出并计算出机器人工作空间容积。在本文的另一部分介绍了两种计算机器人工作空间的性能指标,最后用几个机器人的结构参数进行计算和讨论。

基于工程地质力学的岩土工程加固理论、技术与实践

In the engineering reinforcement of-rock and soil mass, engineers must consider how to obtain better reinforcing effect at the cost of less reinforcing expense, which, in fact, is the aim of reinforcement design. In order to accomplish the purpose, they require not only researching the material used to reinforce and its structure, but also taking into account of several important geological factors, such as the structure and property of rock and soil mass. How to improve the reinforcing effect according to engineering geomechanical principle at the respect of the reinforcement of engineering soil and rock mass is studied and discussed in this paper. The author studies the theory, technology and practice of geotechnical reinforcement based on engineering geomechanics, taking example for the soil treatment of Zhengzhou Airport, the effect analysis of reinforcement to the slope on the left bank of Wuqiangxi Hydropower Station and the reinforcing design of the No. 102 Landslide and unique sand-slide slope on the Sichuan-Tibet Highway. The paper is comprised of two parts for the convenience of discussion. In the first part, from the first chapter to the fifth chapter, trying to perform the relevant research and application at the viewpoint of soil mass engineering geomechanics, the author mainly discusses the study of reinforcing soft ground soil through dynamical consolidation and its application. Then, in the second part, from the sixth chapter to the eleventh chapter, the study of new technologies in the rock slope reinforcement and their application are discussed. The author finds that not only better reinforcing effect can be gained in the research where the principle and method of rock mass engineering geomechanics is adopted, but also new reinforcing technologies can be put forward. Zhengzhou Airport is an important one in central plains. It lies on Yellow River alluvial deposit and the structure of stratum is complex and heterogeneous. The area of airport is very large, which can result in differential settlement easily, damage of airport and aircraft accident, whereas, there are no similar experiences to dispose the foundation, so the foundation treatment become a principal problem. During the process of treatment, the method of dynamic compaction was adopted after compared with other methods using the theory of synthetic integration. Dynamic compaction is an important method to consolidate foundation, which was successfully used in the foundation of Zhengzhou Airport. For fill foundation, controlling the thickness of fill so as to make the foundation treatment can reach the design demand and optimum thickness of the fill is a difficult problem. Considering this problem, the author proposed a calculation method to evaluate the thickness of fill. The method can consider not only the self-settlement of fill but also the settlement of the ground surface under applied load so as to ensure the settlement occurred during the using period can satisfy the design demand. It is proved that the method is correct after using it to choose reasonable energy of dynamic compaction to treat foundation. At the same time, in order to examine the effect of dynamic compaction, many monitor methods were adopted in the test such as static loading test, modulus of resilience test, deep pore pressure -test, static cone penetration test and the variation of the pore volume measurement. Through the tests, the author summarized the discipline of the accumulation and dissipation of pore pressure in Yellow River alluvial deposit under the action of dynamic compaction, gave a correct division of the property change of silt and clay under dynamic compaction, determined the bearing capacity of foundation after treatment and weighted the reinforcing effect of dynamic consolidation from the variation of the soil particle in microcosmic and the parameter of soil mass' density. It can be considered that the compactness of soil is in proportion to the energy of dynamic compaction. This conclusion provided a reference to the research of the "Problem of Soil Structure-the Central Problem of Soil Mechanics in 21 Century ". It is also important to strengthen rock mass for water conservancy and electric power engineering. Slip-resistance pile and anchoring adit full of reinforced concrete are usually adopted in engineering experience to strengthen rock mass and very important for engineering. But there also some deficiency such as the weakest section can't be highlighted, the monitor is inconvenient and the diameter of pile and adit is very large etc. The author and his supervisor professor Yangzhifa invented prestressed slip-resistance pile and prestressed anchoring adit full of reinforced concrete, utilizing the advantage that the prestressed structure has better anti-tensile characteristic (this invention is to be published). These inventions overcome the disadvantages of general slip-resistance pile and anchoring adit full of reinforced concrete and have the functions of engineering prospecting, strengthening, drainage and monitor simultaneous, so they have better strengthened effect and be more convenient for monitor and more economical than traditional methods. Drainage is an important factor in treatments of rock mass and slop. In view of the traditional drainage method that drainage pore often be clogged so as to resulted in incident, professor Yangzhifa invented the method and setting of guide penetration by fiber bundle. It would take good effect to use it in prestressed slip-resistance pile and anchoring adit full of reinforced concrete. In this paper, the author took example for anchoring adit full of reinforced concrete used to strengthen Wuqiangxi left bank to simulate the strengthened effect after consolidated by prestressed slip-resistance pile, took example for 102 landslide occurred along Sichuan-Tibet highway to simulate the application of slip-resistance pile and the new technology of drainage. At the same time the author proposed the treatment method of flowing sand in Sichuan-Tibet highway, which will benefit the study on strengthening similar engineering. There are five novelties in the paper with the author's theoretical study and engineering practice: 1. Summarizing the role of pore water pressure accumulation and dissipation of the Yellow River alluvial and diluvial soil under the action of dynamical consolidation, which has instructive significance in the engineering construction under the analogical engineering geological conditions in the future. It has not been researched by the predecessors. 2. Putting forward the concept of density D in microcosmic based on the microcosmical structure study of the soil sample. Adopting D to weight the reinforcing effect of dynamic consolidation is considered to be appropriate by the means of comparing the D values of Zhengzhou Airport's ground soil before with after dynamically consolidating reinforcement, so a more convenient balancing method can be provided for engineering practice. 3. According to the deep research into the soil mass engineering geology, engineering rock and soil science, soil mechanics, as well as considerable field experiments, improving the consolidating method in airport construction, from the conventional method, which is dynamically compactmg original ground surface firstly, then filling soil and dynamically layer-consolidating or layer-compacting at last to the upgraded method, which is performing dynamical consolidation after filling soil to place totally at the extent of the certain earth-filling depth. The result of the dynamical consolidation not only complies with the specifications, but also reduces the soil treatment investment by 10 million RMB. 4. Proposing the method for calculating the height of the filled soil by the means of estimating the potential displacement produced in the original ground surface and the filled earth soil under the possible load, selecting the appropriate dynamically-compacting power and determining the virtual height of the filled earth soil. The method is proved to be effective and scientific. 5. According to the thought of Engineering Geomechanics Metal-Synthetic Methodology (EGMS), patenting two inventions (to the stage of roclamation, with Professor Yang Zhi-fa, the cooperative tutor, and etc.) in which multi-functions, engineering geological investigation, reinforcement, drainage and strength remedy, are integrated all over in one body at the viewpoint of the breakage mechanism of the rock slope.

Intelligence in Scientific Computing

Combining numerical techniques with ideas from symbolic computation and with methods incorporating knowledge of science and mathematics leads to a new category of intelligent computational tools for scientists and engineers. These tools autonomously prepare simulation experiments from high-level specifications of physical models. For computationally intensive experiments, they automatically design special-purpose numerical engines optimized to perform the necessary computations. They actively monitor numerical and physical experiments. They interpret experimental data and formulate numerical results in qualitative terms. They enable their human users to control computational experiments in terms of high-level behavioral descriptions.

Transition Space

Informal causal descriptions of physical systems abound in sources such as encyclopedias, reports and user's manuals. Yet these descriptions remain largely opaque to computer processing. This paper proposes a representational framework in which such descriptions are viewed as providing partial specifications of paths in a space of possible transitions, or transition space. In this framework, the task of comprehending informal causal descriptions emerges as one of completing the specifications of paths in transition space---filling causal gaps and relating accounts of activity varied by analogy and abstraction. The use of the representation and its operations is illustrated in the context of a simple description concerning rocket propulsion.

Quantitative Inference in a Mechanical Design Compiler

This paper presents the ideas underlying a program that takes as input a schematic of a mechanical or hydraulic power transmission system, plus specifications and a utility function, and returns catalog numbers from predefined catalogs for the optimal selection of components implementing the design. It thus provides the designer with a high level "language" in which to compose new designs, then performs some of the detailed design process for him. The program is based on a formalization of quantitative inferences about hierarchically organized sets of artifacts and operating conditions, which allows design compilation without the exhaustive enumeration of alternatives.

Automated Acquisition of Evolving Informal Descriptions

The Listener is an automated system that unintrusively performs knowledge acquisition from informal input. The Listener develops a coherent internal representation of a description from an initial set of disorganized, imprecise, incomplete, ambiguous, and possibly inconsistent statements. The Listener can produce a summary document from its internal representation to facilitate communication, review, and validation. A special purpose Listener, called the Requirements Apprentice (RA), has been implemented in the software requirements acquisition domain. Unlike most other requirements analysis tools, which start from a formal description language, the focus of the RA is on the transition between informal and formal specifications.