中介命题演算系统MP^M的公理完备集

本文基于中介逻辑命题演算系统MP^M构造了一个公理集合，证明了该公理集合的完备性。该公理集合中的公理均是由等式的形式给出，可以方便地对MP^M、MF^M系统上的等值公式进行推导和证明。本文还讨论了该公理集合在不完全信息数据库查询优化上的应用。     

基于CCS模型的半智能回溯

本文提出了以逻辑式程序设计语言的与并行执行模型CCS为基础的半智能回溯方法,解决了分布式并行处理问题和通信问题,不仅提高了逻辑式程序设计语言的执行功效,又保证了语义的正确性与完备性。     

确定性进程的单向模拟

本文主要讨论了确定性进程单向模拟,与R.Milner的双向模拟相比,本文定义的模拟是单方向的。我们给出了确定性进程的转换规则,并证明了确定性进程单向模拟的正确性与完备性。同时也讨论了单向模拟的转换规律,并把单向模拟看作是一个特定函数的不动点。最后我们讨论了单向模拟的分层性,并且对单向模拟与双向模拟作了比较,证明了双向模拟可以由两个单向模拟组成。     

关于NC程序正确性校验的仿真研究

本文介绍的是作者采用二维图形技术开发的一个仿真系统，旨在通过模拟刀具切削零件的路径、检验ＮＣ程序的正确性。文章首先进行了系统开发的需求分析，继之介绍了系统所具有的功能，最后讨论了该系统所具有的一些特点和独到之处。     

基于集团的系统级故障诊断研究

本文首次在系统故障研究域提出了集团的概念，讨论了集团的性质，并研究了基于集团的系统故障诊断的可诊断特性。本文还详细论述了基于集团的一步ｔ可诊断算法及求集团算法，并论证了算法的正确性与完备性。     

APA：类比自动程序设计系统

自动程序设计系统APA使用类比推理技术,向过去经验学习编写新的LISP程序.本文首先给出了它的知识表示和系统结构,然后讨论怎样发现与新问题相似的已解问题,怎样沿着相似推导构作新问题的程序.APA是[1,2]中类比推理理论的一个实验系统.     

矩阵束的稳定凸组合与完备性的等价关系

矩阵束存在稳定凸组合是其有分段公共Lyapunov函数的一个充分条件．矩阵束的完备性是切换系统为稳定且存在切换控制函数一个充分条件．本文讨论了在一定条件下矩阵束稳定凸组合的存在性和相应矩阵束的完备性的等价关系，给出切换系统的分段Lyapunov函数的构造方法．并分析了自治切换系统的稳定性。     

一个面向C和Fortran数值程序的静态分析工具

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。     

空值环境下广义连接依赖（NGJD）及推导规则的研究

本文给出了空值环境下广义连接依赖强保持、弱保持的概念。讨论了它们的推导规则，证明了各推导规则在强保持、弱保持条件下的存在性，以及相应的完备性结论。     

空值环境下广义连接依赖及推导规则的研究

本文给出了空值环境下广义连接依赖强保持，弱保持的概念。讨论了它们的推导规则，证明了各推导规则在强保持，弱保持条件下的存在性，以及相应的完备性结论。     

FPNN:优化的过程神经网络模型及其应用

利用既定条件下过程神经元与傅里叶神经元的等价性,提出一种优化的过程神经网络模型FPNN,并对等价性进行了证明。FPNN网络在保持了过程神经网络模型表达能力和预测准确率的同时,继承了FNN的优点,大大提高了模型的效率。     

面向嵌入式软件开发的UML到Simulink模型转换方法

模型驱动开发及其关键技术模型转换是近年来软件工程领域研究的热点。在嵌入式软件开发早期,不仅需要对设计模型进行静态分析,更需要对其进行动态仿真,验证系统设计的正确性。如何把设计模型和仿真模型无缝连接起来是工业部门亟待解决的问题。深入调研了UML和Simulink模型转换研究现状,详细分析了模型驱动开发中模型转换的相关技术,提出了一种UML到Simulink的模型转换方法,设计了UML元模型、Simulink元模型,撰写了UML元模型到Simulink元模型的映射规则。最后选取自动驾驶仪系统的飞行控制软件作为案例,验证了该方法的正确性。该方法能实现UML和Simulink两种异构模型同构化,提高嵌入式软件开发效率,丰富并且完善模型驱动开发,也为飞行控制系统、高速铁路控制、机载航电系统等嵌入式软件开发提供了技术支持。     

形式化构件规约自动生成中的演化转换

基于软件体系结构的开发将是未来大型、复杂软件开发的主要技术,而构件是该方法的基础。形式化构件规约对构件的功能描述、分类和检索有重要意义。文中给出了一种用于形式化构件规约自动生成的转换方法即演化转换,对该方法的转换过程、转换规则提取、表示及主要转换算法进行了详细说明,并对规约的完整性和转换的正确性进行了探讨。最后,还对该方法的实现系统及其特点进行了简要介绍。演化转换能较好地控制转换粒度和跨度,对转换正确性和规约完整性也有一定的保证,在转换过程中实现了规约的垂直重用,使构造的模型和规约对需求变化有一定的适应性。     

NDAUTO：An Experimental Software Automation System

This paper describer the design and implementation of an experimental software automation system(NDAUTO).By combining the transformational and procedural approaches in software gutomation,the system can tansform software unctional specifications written in a graphical specification language GSPEC to executable programs sutomatically,The equivalence between a specification and its corresponding program can be guaranteed by the system,and the correctness of the specification can also be validated.The main new points of the work lie in the design of the specification languange,the transformation mechanism and the correctness validation of the specification.     

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换，形式化推导出可读性好、效率高的递推的最小生成树算法，简化了算法程序设计和正确性证明的过程，有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。     

An Admissibility-Based Operational Transformation Framework for Collaborative Editing Systems

Operational transformation (OT) as a consistency control method has been well accepted in group editors. With OT, the users can edit any part of a shared document at any time and local responsiveness is not sensitive to communication latencies. However, established theoretical frameworks for developing OT algorithms either require transformation functions to work in all possible cases, which complicates the design of transformation functions, or include an under-formalized condition of intention preservation, which results in algorithms that cannot be formally proved and must be fixed over time to address newly discovered counterexamples. To address those limitations, this paper proposes an alternative framework, called admissibility-based transformation (ABT), that is theoretically based on formalized, provable correctness criteria and practically no longer requires transformation functions to work under all conditions. Compared to previous approaches, ABT simplifies the design and proofs of OT algorithms.     

An Alphard Specification of a Correct and Efficient Transformation on Data Structures

In this paper we study the problem of designing and specifying standard program components applicable to a wide variety of tasks; we choose for this study the specific problem domain of data structures for general searching problems. Within this domain Bentley and Saxe [1] have developed transformations for converting solutions of simple searching problems to solutions of more complex problems. We discuss one of those transformations, specify precisely the transformation and its conditions of applicability, and prove its correctness; we accomplish this by casting it in terms of abstract data types–specifically by using the Alphard form mechanism. The costs of the structures derived by this transformation are only slightly greater than the costs of the original structures, and the correctness of the transformation definition together with the correctness of the original structure assure the correctness of the derived structure. The transformation we describe has already been used to develop a number of new algorithms, and it represents a new level of generality in software engineering tools.     

Recursive Program Optimization through Inductive Synthesis Proof Transformation

The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality.     

MSK调制技术研究

基于System View仿真系统,研究了一种典型的恒包络调制技术―最小移频键控(MSK),分析了MSK信号的正交调制和解调原理,以及MSK调制技术的特点,利用System View对MSK系统进行了仿真模拟,并对仿真结果进行了分析和总结。