归纳证明在类型理论中的应用研究

通过类型理论使得程序语言在静态可以检查是否出错,这给程序语言带来许多优势。类型理论中的重要性质包括:弱化规则、删除规则、强化规则等。首先给出了结构归纳法、良基归纳法、规则归纳法和余归纳法的形式化定义。在给出PA4WS进程代数的语法、语义的基础上给出了其类型定义。在此基础上给出了归纳法在PA4WS类型理论性质证明的应用。     

基于本体的多无人机系统语义互操作方法

引入基于领域本体的语义模型形式化建模方法,提出了多无人机交互描述的语义描述模型方法和交互配置的语义增强方法.设计了无人机本体UAV O和服务描述本体UAV OS,在OWL S（Ontology Web Language for Services）基础上扩展服务动态特性等的描述,可以为服务质量、服务状态和服务关系提供语义描述;扩展了对多无人机任务和动态配置、组合所需控制结构等的描述.为了实现多无人机应用配置的自动化和动态性,基于本体的语义增强方法可以用于配置管理,在匹配中引入高层次的语义增强匹配,对多无人机交互配置处理进行语义增强.在无人机综合仿真环境中进行了验证,结果表明,提出的基于本体的语义互操作方法能有效地支持多无人机应用交互和集成.     

基于SPIN的BPEL4WS建模与验证研究

Web服务组合研究领域的一个重要问题是如何形式化描述Web服务组合,验证服务组合的正确性,Web服务组合的形式化模型可以用来检查和验证Web服务组合以保证组合的正确性.文章使用模型检查工具SPIN对目前普遍使用的Web服务组合规范BPEL4WS (Business Process Execution Language for Web Services,Web服务业务流程执行语言)模型进行了验证,给出了BPEL4WS语法到Promela形式化模型的转换方法,最后通过一个实例对BPEL4WS表示的服务组合模型的安全性、活性和有界性等特性进行了验证分析,从而给出了基于SPIN的BPEL4WS表示的Web服务组合模型验证的方法.     

基于WS-CDL的图形化标识语言研究与建模工具的实现

Web服务编排描述语言(WS-CDL)从全局的视角定义了Web服务参与方之间的协作和交互.然而,作为一个业务流程建模语言,WS-CDL规范缺乏对应的图形化标识标准,导致业务人员无法方便地编排流程.为此,设计了一套图形化模型标记WS-CDL-N,该标记与WS-CDL一一对应.并在此基础上,使用GMF框架实现了WS-CDL...     

基于ＯＯＺＳ的ＵＭＬ类图形式化描述及其应用

统一建模语言UML是一种面向对象分析和设计过程中重要的建模工具。但由于UML缺乏精确的形式化语义,不利于对其所描述的需求进行进一步分析和验证。这一点上,形式化方法可与之互补。基于此,本文采用一种面向对象的、基于Z的扩展语言OOZS———结构化面向对象形式规格说明语言,对UML的类图进行了形式化描述,寻求一种在软件设计与系统建模过程中UML到OOZS的映射与转换机制,最后给出一个基于OOZS的UML类图的形式化描述实例,结果表明本文的研究工作在实践中是可行的。     

OCL 2.0表达式语义学比较研究

从语法、语义域和语义映射三个方面,给出了基于UML元模型和形式化的OCL表达式语义描述.并探讨了OCL表达式上下文、OCL表达式赋值环境的概念.在OCL表达式语义的形式化描述中,定义了对象模型和OCL表达式语法,给出OCL表达式语义解释和OCL后置条件表达式的语义解释.通过对OCL表达式语义二种描述方法比较,可以看到OCL表达式语义学描述的关键是反映OCL表达式本质的语法描述.     

基于二元关系的语义Web的建立

为了便于机器理解和提高网络资源的利用率提出了语义Web .基于二元关系讨论了语义Web的建立过程 ,具体给出语义Web中相关语义的形式化定义 ,并基于此给出了语义描述和挖掘方法 ,进行了集合相关语义的完备性的证明 .为了语义Web能应用于实际网络中 ,给出了语义拓展方式的定义 ,继而完成语义Web的形式化定义 ,给出语义Web的整体模型 .最后 ,给出了若干用于检验语义有效性的方法 ,以进一步提高语义Web的实用性 ,至此可创建相对完整的语义Web .     

UML 2.0的形式化语义研究

由于UML 2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证.基于此,在描述UML 2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML 2.0顺序图和状态图之间的模型转换,也为使用UML和形式化方法相结合描述软件体系结构的交互行为奠定了基础.     

本体定义及本体代数

基于现有的本体定义,采用函数式描述语言精确定义了本体建模基元,给出一种新的本体形式化描述,并给出了本体间近义关联的定义,在新本体形式化描述和本体间近义关联定义的基础上,提出一种具有封闭性的本体代数定义,同时结合函数式描述语言,给出了其形式化描述.     

基于Petri网的语义Web服务组合模型

针对现有的语义Web服务组合的描述语言本身缺乏明确的操作语义,无法准确的描述其组合流程的问题,就此提出了一种基于Petri网的语义对Web服务组合流程进行形式化建模的方法,并通过实例验证了该方法的有效性和可行性.     

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

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

基于状态反馈的四轮转向汽车LQR优化控制

为了提高汽车的操纵稳定性,以4轮转向(4WS)汽车为研究对象,建立了2自由度系统的数学模型和状态方程。并以横摆角速度和侧偏角为优化目标,设计了线性二次型调节器(LQR)。通过质心侧偏角和横摆角速度的共同反馈,控制汽车后轮转角,实现4WS控制。在MATLAB/Simulink环境下完成了传统前轮转向汽车、零侧偏角比例控制及LQR控制的4WS汽车仿真。结果表明,相对于其他控制策略,基于状态反馈的LQR优化控制能够改善汽车的操纵稳定性,但不能够既将汽车的质心侧偏角降到基本为零,同时又保证横摆角速度处于理想状态。因此,汽车动力学集成控制将是未来汽车发展的重要方向。     

形式语义描述方法研究进展与评价

程序设计语言形式语义描述技术在1990年代进入新一轮发展高潮,它对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及安全协议形式化描述、分析验证与设计等都有着重要的意义。但不同于成熟统一的形式化语法描述技术,语义的形式描述技术尚处于蓬勃发展和多种技术并存时期。首先回顾形式语义描述方法的研究发展史;然后通过实例介绍当前主要的语义形式描述方法;最后给出这些方法的评价标准和比较结果,并指出最有发展潜力的语义描述方法,以及将来的发展方向。     

WS-CDL测试路径的生成与排序

为了找出WS-CDL组合流程中存在的错误,减少软件维护产生的开销,提出一种基于控制流图生成测试路径的方法,用于对WS-CDL进行测试.首先解析WS-CDL文档,根据元素特点生成各类节点,并根据流程结构确定节点的源节点和目标节点;然后通过在源节点和目标节点间添加有向边构造成控制流囹;最后通过遍历控制流图生成所有可能的测试路径.测试路径中覆盖的WS-CDL元素越多,则发现的错误数也可能越多.为提高发现错误的效率,提出了2种基于路径中元素数量的排序算法,对路径的执行顺序进行排序.实验结果表明,将测试路径按路径中未被覆盖的元素总数降序排列,可以更快地发现错误.     

为功能而形式——P.Sgall的FGD语言理论框架与TFA

介绍并讨论捷克Charles大学Petr Sgall教授主创的、对语言进行功能生成描述的FGD形式化理论框架。该理论框架与布拉格学派的功能句法系统地融合,克服了乔姆斯基的生成语法在处理自由词序方面的缺陷。FGD形式化理论框架目前已应用于捷克国家语料库,并与美国以Barbara Partee为代表的形式语义学派融合。在国内该理论框架还未曾有过细致深入的介绍与讨论,可以填补这方面的空白。     

一种Verilog的操作语义

用形式化的方法描述了硬件描述语言Verilog的语法和语义,建立了一个Verilog的操作语义模型。分别用二元组和四元组描述Verilog非并发和并发成分的状态,刻画了不同语句的状态转换规则,并用实例描述了并发程序的执行过程,证明了该操作语义模型的正确性。     

一种形式语言代数模型

针对形式语言研究的国内外现状,对形式系统规约描述语言的数学模型进行了初步探讨,建立了一种形式语言的代数模型,依据软件重用的思想及转换语义的方法提出了语言重用的概念,根据软件工程分层设计原则构建了形式语言族模型.该模型在不同层次上描述复杂形式系统软件规约的抽象表达程度,适于复杂形式系统的开发与测试.此外,文中应用范畴理论...     

哥德巴赫猜想证明及验证

在《前沿科学》2011第三期《揭开素数神秘的面纱》一文中得到PA数列（Prime Arrav）及其性质后。再将该PA数列分列直角坐标第1象限X、Y轴上顺序方型相加,得X轴各素数住与该PA数列结构相似的“PA和数列”,用“边带型相加移位还原”按数学归纳法先证明,边带型相加移位还原的两奇素数和连续的范围比组合最大奇素数所在的方形范围越来越更大,两奇素数和进入奇数积连续段的每个偶数的能力越来越更强,全部进入各范围内奇数积连续段的Oj1速度越来更快;再用满足莫比乌斯带（Moebius strip）转换等反证验算,完成整数→∞,在任X×X方型范围内（X≥3奇数）哥德巴赫猜想成立。