论形式系统的多样性

形式系统在类型上包括公理系统和自然推理系统,在构成要件上包括的形式语言和演绎装置.构造者的哲学背景、构造形式系统的理论对象和目的不同,所采用的形式语言和演绎装置就可能不同,因而,构造出来的形式系统就多种多样,在不同的系统内证明同一个定理也表现为不同的公式系列.形式系统的形式语言和演绎装置为我们界定了形式证明的工具、出发点和依据,同时语义也包含了构造者构造形式系统的理论对象和目的,离开具体的形式系统去谈论或者证明一个定理,将会导致逻辑的失范.     

一种基于范畴论方法的形式语言模型

针对形式语言理论研究的国内外现状,建立了一种基于范畴论方法的形式语言模型,在范畴论的形式化框架内论证了该形式语言模型与其生成范畴间的内在联系,利用范畴论的素描工具结合实例对该模型进行了应用,通过分析比对说明了该模型在保持形式语言语义完整性方面的优势,为形式语言的建模理论研究提供了一种基于范畴论方法的新思路,为形式系统结构设计与形式语言理论框架的研究提供一个高效、便利的形式化理论框架.     

基于XML的类规约实现和重用研究

将XML技术应用到类规约描述和重用中,提出了一种基于XML的类规约重用方法.使用XML描述可重用的类规约,设计类规约重用的一般流程以及需要遵守的准则,然后在类规约库中查找符合需求的类规约进行重用.实践证明,重用XML描述的类规约可以使软件分析效率得以大幅提高.     

上下文无关文法的可视化描述

上下文无关文法借助有限规则集和递归手段实现语言生成问题的刻画.这一形式系统多以符号串集形式呈现,并因递归技术的应用而渐变复杂,晦涩难懂.文章探讨其可视分析问题,涉及文法到有限状态变迁系统的构造、理论证明和应用方法.这项工作不仅有助形式系统各要素间的关系的直观刻画,而且为结构化推导分析、语义重用奠定基础.     

向量值一阶逻辑及其可靠性定理

讨论了向量值一阶逻辑形式系统。通过对于在智能系统多认知环境下事物逻辑性质的分析,把逻辑真值推广到一个n维向量。在对于向量值命题逻辑形式语言建立可靠性定理与完备性定理的讨论基础上,这里进一步建立了向量值一阶逻辑形式系统,证明了它的可靠性定理。     

形式规约模式及其重用技术研究综述

设计模式的形式规约描述的研究对于设计模式的广泛重用具有重要意义.规约模式就是用某种形式化语言表示的设计模式.文章从模式定义、重用机制、可用工具、方法可用性等角度分析比较了几种主要的设计模式形式化方法.最后讨论了当前存在的问题及其发展趋势。     

递归问题的一种直观执行模型

针对递归过程的直观理解问题,提出了一种形式语言。通过该形式语言,可在对递归程序宏观仅有所了解的基础上构造出直观执行模型。实例证明,此直观执行模型能有效地使复杂递归过程具体化。     

一种分布式制造信息系统控制性能的研究方法

提出一种解决Ramadge-W onham监控理论在研究分布式制造信息系统控制性能时存在的形式语言的物理意义不直观、运算复杂且计算量大等问题的方法.该方法将信息单元的自然语言描述形式化,写出形式语言的文法,引入布尔矩阵约束,由该文法产生的信息单元自动机模型满足必要的控制性能要求.最后以某企业自动生产线中的装配机器人为例,应用该方法研究其自动机模型的控制性能.结果显示,该方法计算简单,形式语言的物理意义直观,值得在制造领域中推广.     

基于层次结构的参数化装配模型重用机制

针对复杂装配参数化模型设计资源重用问题,提出了基于层次结构的参数化装配模型重用机制.该机制由装配-零部件参数化层次建模、主控-细节参数的层次引用、几何链接层次更新、用户导航界面层次设计和基于层次匹配的可视化自动测试框架构成.通过该机制在模具设计平台上的应用实施,提升了装配重用的效率.     

复杂结构零件的初始化设计知识模型构建

为了实现设计重用,提出了一种面向复杂结构零件的初始化设计知识模型构建方法.采用功能特征分解对复杂结构零件进行了从功能到其映射结构的逐层解析,构建了功能结构设计矩阵,研究了各级功能结构的设计流程规划方法.以特征分解树为框架,研究了面向对象的表示方法对各级功能结构设计支撑知识的模块化封装,最终实现了初始化设计知识模型的构建.应用结果表明,在汽车发动机气缸体设计知识模型的构建中,该方法可有效地实现对其设计知识的条理性重用.     

软件的面向对象表示及在软件分析中的应用

通过从面向对象的角度理解实现软件的形式语言,可建立软件结构的对象模型,文章描述了自动建立软件结构对象模型的方法和过程。最后,结合在软件分析中的应用,讨论了该模型的实现及其与软件分析工具的结合。     

UML视图的一种形式化模型及其分析

UML是一种得到广泛应用的系统建模语言，但是由于它缺乏形式化语义和严格的推理机制，从而影响了系统建模的准确性和开发效率。TCOZ是一种将Object—Z和TCSP相结合的形式化语言，具有丰富的建模能力。基于TCOZ，本文建立了UML视图的一种形式化模型，对类图和协作图等提出了转换规则，使得TCOZ中的推理可用于分析UML视图。通过某学校信息系统的实例，阐述了UML视图的形式化建模方法和分析技术。     

UML 顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。     

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

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

PRAPS：一个用于自动程序设计的问题表示系统

提出了使用领域知识与专家系统技术形成形式问题模型的方法，并在ＰＲＡＰＳ系统中得以实现。这一方法的应用，使用户仅以自然语言形式提出问题，经ＰＲＡＰＳ系统，最终形成描述问题的形式化模型，从而为自动设计解决问题的程序奠定了基础。     

基于场景的形式化测试模型生成方法

在复杂的Web应用软件中,如何有效地实现自动化测试是当前软件测试研究中的热点与难点.使用统一建模语言（unified modeling language,UML）状态图对Web应用软件的行为建模,利用已有的方法将已建好的模型形式化成有限状态机(finite state machine,FSM);然后使用UML顺序图表示场景,通过使用场景规约系统行为,最终得到约简后的形式化测试模型用以实现自动测试.     

一种基于Object-Z的面向方面建模方法

提出一种基于Object-Z的形式化面向方面建模语言及其建模方法。方面规范提供了观察基本模块和方面模块的行为、描述它们相互关系的手段,编织机制将两类模块系统地集成为一个完整的系统模型。该方法能有效地简化系统建模,提高系统模型的可复用性,也为进一步验证系统性质提供了理论基础。     

基于TCOZ的UML用例图的形式化模型

基于TCOZ,本文建立了UML视图的一种形式化模型,不仅为UML提供了一种精确的数学描述,也为其正确性分析和验证奠定了基础。