基于模型检验的构件验证技术研究进展

模型检验以其自动化程度和完备性高、与构件技术互补性强等特点,在软件构件可信性质的分析和验证中发挥着日益重要的作用.将基于模型检验的构件验证方法分为基于系统规约模型的验证和基于源代码的验证,分别对其研究现状和发展动态进行了详细的综合评述.首先对模型检验与构件可信性质验证的关系进行了探讨,接着对基于SOFA,Fractal,CORBA及各种特定构件模型的验证方法和基于转化思想的源码验证、面向源码的直接验证及面向可执行代码的动态验证方法分别进行了评述.最后,指出了基于模型检验的构件验证技术所面临的主要挑战和未来的发展方向.

构件组装及其形式化推导研究

基于构件的软件工程(component based software engineering,简称CBSE)能够有效地提高软件开发的质量和效率.构件组装和组装推导(compositional reasoning)是CBSE的关键技术.基于软件构件的特点,借鉴进程代数中进程构造的方法,提出6种构件组装机制,能够灵活、简便地集成软件构件,并主张在构件组装的同时进行接口组装,通过生成功能更强、抽象级别更高的复合接口,提高构件组装的抽象级别和粒度.同时,基于Wright的形式化规约软件体系结构的研究,给出了复合构件和复合接口的组装推导算法,为系统行为的形式化分析、验证和仿真奠定了基础.

硬件构件的形式化描述及其组装机制

针对构件化的路由交换平台设计,提出硬件基础构件的抽象模型及其内部处理流程的形式化描述,提取出顺序、并行、分支以及聚合4种原子组装机制,用于构建更高层次的复合构件,并推导出复合构件抽象模型及其处理流程的形式化描述,从而有利于抽象出更大粒度的构件用以组装复杂的硬件平台。

基于自动机的构件实时交互行为的形式化模型

采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义。分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法。时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证。最后,结合具体应用给出了应用示例。

构件行为协议实时性扩展及相容性验证

对复杂实时构件系统行为进行形式化描述和相容性验证,可以有效提高系统的正确性、可靠性。分析了学术界和工业界的主流构件模型及常见时间行为的形式化描述方法,对构件行为协议BP(Behavior Protocol)进行了扩展,提出了时间行为协议TBP(Ti med Behavior Protocol),分析了构件组合中常见的相容性错误类型,给出了基于时间行为协议的构件组合相容性验证算法。TBP应用简洁、方便、易于验证。结合具体例子给出了应用示例。

基于协议的实时构件行为一致性验证

对复杂实时构件系统行为进行形式化描述和一致性验证,可以提高实时构件的可复用性和系统的正确性、可靠性。分析了时间行为协议TBP(Timed Behavior Protocol)及其它学术界和工业界常用的时序行为形式化描述方法,对实时构件替换理论进行了讨论,给出了基于时间行为协议的构件一致性验证算法并对其进行了分析。

一种基于线性逻辑的构件组装方法研究

构件组装是基于构件的软件开发中的一个重要环节.本文利用线性逻辑描述了具有语义信息的构件结构,描述了独立于具体的计算环境、具有普遍适用性的三种构件组装关系,利用定理证明的方法,根据现存构件的描述和构件组装关系自动生成构件组装的方案,并从被适应的构件描述中推导出复合构件的描述,以提高对构件适应过程的描述和分析能力,为构件组装形式化分析、组装正确性的检验提供了保证,并列出了一些值得进一步研究的问题.

可视化部件规格匹配的研究

分析了现有的重用部件的检索及匹配方法，提出了一种可视化重用部件的形式化规格描述，讨论了几种基于规格描述的部件匹配，并阐述了不同种类的部件匹配情况下部件的重用方式（黑盒重用或白盒重用）．

基于排序形式化规格说明的软构件匹配

基于排序形式化规格说明的软构件匹配是检索可重用构件的有效方法 ,在软件复用和库检索中 ,有助于确定一个构件是否可以取代另一个构件或一个构件如何通过修改以满足另一个构件的要求。利用基于排序形式化规格说明来描述软构件的行为 ,并在构件和方法层次上给出多种不同类型的基于排序形式化规格说明软构件匹配的定义 ,及其在构件检索中的应用。

面向构件的系统开发及其形式化

回顾了软件构件与形式化方法的基本概念,介绍了软件构件的形式化,根据典型的面向构件的开发流程和基于形式化方法开发软件的特点,提出了一个基于形式化方法的面向构件的系统开发模型。针对目前面向构件的软件开发形式,提出了一些建议和方向。

基于时序逻辑证明编译优化程序变换的保义性

基于时序逻辑CTL(computation tree logic)的一种扩展CTL-FV对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画,采用含条件重写规则定义了保义语句交换Texch和保义变量替换Tsub,并基于一种归纳证明框架对它们的保义性进行了证明.此外,基于变换Texch对程序基本块内保依赖语句重排的保义性也给出了一种构造性的证明.

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

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

基于T^3BDD的动态模型检查

ＪａｖａＢｅａｕｓ是一种组件标准．该文定义了ＪＢＤＬ（ＪａｖａＢｅａｎｓｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）语言，用于描述组件语义约束规范．为了检测ＪａｖａＢｅａｎｓ组件语义约束与其实现之间的一致性，文章给出了一种基于Ｔ3ＢＤＬ公式的三值语义和模型的抽象化动态模型检查方法、文章重点介绍了利用ＴＢＤＤ（３－ｔｅｒｍｉｎａｌｂｉｎａｒｙｄｅｃｉｓｉｏｎｄｉａｇｒａｍ）的符号化动态模型检查方法．

荷兰国旗问题的形式化推导及其多态性实现

讨论了程序功能规约变换和算法程序的形式化技术。通过功能规约变换,可以较自然地获得问题求解的递推关系,对荷兰国旗问题的求解过程显示了形式化推导在获得高效和正确的算法程序中的作用。最后,给出了问题求解的多态性实现。

构件适应和组装的形式化语义描述

构件适应技术是基于构件的软件工程中一个很难解决的问题,分析了三种构件适应结构的应用条件,采用了形式化语义的方法描述和推导了与构件以及构件适应相关的问题,根据构件描述与应用需求描述动态地选择不同的适应层次来适应构件,从被适应的构件描述中推导出复合构件的描述,为构件适应的形式化分析、组装正确性检验提供了保证,并列出了一些值得进一步研究的问题。

基于算法框架的可重用部件设计与实现

对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。

分划递推法在Hanoi塔问题上的应用

采用分划递推法通过功能归约变换,形式化推导和证明H ano i塔问题中圆盘的移动规律,从而推导出结构清晰、可读性好、效率高、占用存储空间与圆盘个数无关的非递归算法,算法比较分析地显示出形式化推导在获得高效和正确性的算法程序中的作用.相关算法在UN IX平台下用C语言进行实现.

基于Larch/C的组件形式规范匹配

主要阐述了一种组件的形式规范匹配方法，以Larch家族中的Larch/C作为语言工具，详细讨论了组件的功能匹配，最后借助于工具Larch Prover（LP）并通过实例描述了功能匹配的证明过程。

TCBV:一种构件时序行为建模与相容性验证工具

利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。

多态性构件及其代数规范

可复用构件往往需要引入多态性支持,但是这给构件的形式化定义带来很多困难。采用代数规范系统来定义空间几何实体构件的组织结构及其行为特征,可以有效的支持构件的数据和行为多态性。在多层次的代数规范理论基础上,引入了构件的参数化多态和包含多态,建立了空间几何的实体多态性构件系统,实例表明了系统对于数据和行为多态性方面的有效性。