基于B方法的Web Service组合描述和验证方法

对于Web Service及其组合来说，保证其组合的正确性是十分必要的。B方法是一个基于模型的形式化方法，有很强的结构化机制和很好的工具支持，对于建模和软件验证是一种有效的方法。该文基于B方法对Web服务及其组合进行了形式化建模，并能够利用B方法相对成熟和完善的模型检查工具，来完成模型的正确性验证。     

基于UML状态机与B方法的高可信嵌入式软件开发

提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案：以软件的UML状态机模型为起点，将其转换为B抽象模型并在B工具中验证该模型的一致性，然后遵循B模型逐步精化的开发规则，利用B方法的精化正确性验证功能，得到系统的可靠的实现模型，最后借助B工具自动生成C代码。实例分析表明，这套方法可以提高尚可信嵌入式软件的开发验证效率。给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则。     

参数域上的任意次B-样条有限元法

该文给出了在参数域上应用任意次B－样条有限元法的方法，文中首先介绍了任意次B－样条基的建立方法，并给出了一般的实施步骤；然后又以三次B－样条有限元法为例，求解了2臂圆锥对数螺旋天线的电流分布，其结果说明了该方法的有效性，此外，该文还在更一般的意义上提出了在参数域及交换域上进行剖分的思想。     

基于ARM微处理器和uClinux的串行通信的设计与实现

介绍了ARM微处理器、嵌入式uClinux系统及开发环境的建立，尤其是提出了基于S3C4510B微处理器和uClinux的串行通信的设计方法，其结果正确、可靠。本文详细论述了该方法的具体实现。     

基于目标的软件可信性需求规约方法研究

高可信系统的软件规模不断扩大，其关键是分析并定义一致的可信需求描述，直接影响到需求规格说明的质量，进而影响到最终软件产品的质量。在目前公认的非功能需求规约框架的基础上，利用B抽象机理论，结合面向目标的规约方法，建立了一种可信性需求的分析与定义方法，即软件可信剖面。该方法可应用于UML，利用B抽象机理论，为可信性需求模型的定理化证明奠定了基础。     

B样条曲线曲面GC2扩展

提出了一个扩展B样条曲线曲面的新方法，扩展B样条曲线曲面的关键是为新增加的点确定节点值，新方法的基本思想是：首先，B样条曲线和扩展部分在连接点处满足GC^2连续，用能量极小化方法确定扩展部分的曲线形状，通过对曲线重新参数化使两部分曲线满足C^2连续，进而确定新增加点的节点值，新B样条曲线的控制点由一个显式递推公式计算，原B样条曲线和扩展后的部分合在一起形成一条新的B样条曲线，新的B样条曲线满足原B样条曲线和扩展的点，文章还讨论了运用该方法进行B样条曲面扩展，且以实例对新方法与其它方法进行了比较，结果表明新方法的光顺性得到了明显改善，曲率变化更平坦，且有较小的旋转数指标。     

基于Internet的电子单证研究与开发

EDI由于其标准化、安全性高等原因已经成为B2B贸易的主要方式，但是传统EDI的接入费用昂贵，一般的中小企业很难介入，本文提出了基于Internet的EDI单证的实现方法，并开发具体实现。     

数据交换技术在B2B电子商务中的应用和发展

在B2B电子商务解决方案中，如何交换参与商务活动企业的信息系统之间不同标准的数据是一个重要问题。传统的方法是应用基于增值网VAN的EDI技术，随着Internet的迅速发展，XML技术的日渐成熟，B2B电子商务的数据交换技术出现了新的发展契机。本文分析和比较了应用于数据交换领域的几种主要技术，并提出了一种基于XML的B2B电子商务数据交换的解决模型。     

Web Services在B2B集成中的应用

介绍了Web Services技术，Web Services在实现真正的跨语言、跨平台．跨企业的集成中是非常重要的。着重分析了采用Web Services技术为实现B2B集成带来的优势，并结合具体项目实现B2B集成，讨论了Web Services技术在B2B集成系统中的具体应用方法。     

一种新的均匀样条曲线曲面设计方法

本文根据均匀B样条基函数的de Boor-Cox递推公式提出了一种新的样条曲线曲面设计方法。该方法从满足正性、局部支柱性和权性的初始基函数出发，可构造出具有高阶低次或低次高阶的多项式样条基函数和多种函数类型的样条函数。给出了设计这种样条曲线曲面的几种方法和实例，并对基函数的连续可微性进行了证明。该样条基函数和样条曲线曲面具有和均匀B样条类似的几何性质，且均匀B样条是其特例，可用于曲线曲面的几何造型和样条插值。     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范（程序）的精化。精化演算方法能够通过演算的方式,把规范逐步精化为程序。然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的。形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序。因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索。     

Towards a formal framework for software reuse

It is reasonable to expect that the use of formal methods in software reuse will help improve the practice of this discipline as well as enhance our understanding of its products and processes. We have identified the following technical activities that take place in software reuse as candidates for a formal modeling: representing reusable assets, representing reuse queries, defining matching criteria, defining a storage structure, deriving measures of distance and deriving a calculus of program modification. In this paper we discuss how a simple mathematical model based on set theory and relation theory allows us to capture these activities in a unified, coherent framework.     

典型软件体系结构切片方法的研究

近年来,软件体系结构逐渐成为软件工程领域的研究热点以及大型软件系统与软件产品线开发中的关键技术之一.该文从软件体系结构的主要构成、形式化表示、静态切片和动态切片、前向切片和后向切片以及切片的应用等方面为基本思路,对该领域中已提出的主要研究方案进行了分类阐述和比较分析,总结了其最新研究进展,为下一步的研究提出了新的课题和设想.     

实时系统软件开发过程中形式方法的作用

针对实时系统软件开发的特殊性要求,本文强调形式方法是保证实时系统软件开发正确的一种重要方法。文章首先对形式方法的含义进行了系统的介绍,然后分析了形式方法的三个分支在实时系统软件开发过程中的作用,即形式规约、定理证明、形式验证,并指出了形式方法当前主要应用的能力以及应用的局限性,最后提出了形式方法的一些主要研究方向。     

软件缺陷及其对软件可靠性的影响分析

软件缺陷是软件失效的源头,是影响软件可靠性的重要因素。简述了几种典型的软件缺陷分类方法,结合C++语言,提出了面向程序代码的软件缺陷分类法。采用程序变异方法模拟各类软件缺陷,通过实验,归纳并总结了不同类型的软件缺陷对软件可靠性的影响。     

基于Event-B和Rodin开展形式化软件工程教学

形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可信软件的方法,是软件工程教学的重要补充。     

软件需求的形式化转换模型

需求规范错误是软件设计错误的一大类。该文提出了一个软件需求的形式化转换模型，用来将软件需求分析直接、自动地转换为形式化描述，为需求验证提供帮助，避免软件在需求规范上可能产生的错误。     

一种结合线性时序逻辑和故障树的软件安全验证方法

嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线性时序逻辑和故障树的安全验证方法。该方法运用线性时序逻辑对故障树进行形式化规约,从中抽取出软件安全属性并用时序逻辑公式进行描述,用以支持对安全关键软件的模型检验。最后,以某机载控制系统软件数据处理故障模块的模型检验为例,来说明该方法的有效性和可行性。     

Removing partial parametrization for efficient implementation of functional languages

This paper describes a program transformation technique for functional languages called removing partial parametrization. By transforming functional programs into equivalent ones without partial parametrization, each function is applied to the same number of arguments as its formal parameters. A new method of improving the efficiency of the implementation of functional language is to design the compiler according to the features of the program without partial parametrization. We have used this method in the environment-based implementation of the functional programming language LK. Programs run considerably faster and consume less memory space than traditional ones.     

航空机载嵌入式控制软件需求建模的形式化工程方法

嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDL-MV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。