基于事件驱动的系统级仿真器的操作语义

SystemC是一系统级描述语言.与传统的编程语言相比,它具有一些新的编程特性:延迟的事件通告、延迟事件通告的重载、延迟事件通告的取消以及delta-cycle.研究它的操作语义可以为进一步的形式化方面的研究提供基础.     

混合控制系统及其分析与设计方法

混合控制系统是指那些由实时产了系统和实时数值反馈子系统组成的系统，这类系统的特点是事件变量和时间变量的演化在不同系统内并行，实时地进行，本文基于对混合控制系统以往研究框架的分析，给出了混合控制系统的一个新框架，并提出了混合动态系统的分析和设计方法，混合控制系统的包括系统性能指标的分解，决策子系统的设计和实时数值反馈子系统的设计，其分析则分为离散时间域和离散事件域分析，文中采用了煤气炉系统作为例子说     

基于形式化方法的需求分析

利用形式化规格说明语言——B语言对软件需求进行了严格定义，在严格的数学基础上进行软件开发，以获得更好的软件性能。利用形式化方法的需求分析，有助于发现需求中隐含的不一致性、二义性和不完整性，对其进行更深入精确的理解，从而进行规范化管理。     

Verilog操作语义研究

提出了一个结构化操作语义模型,用于描述Verilog核心子集的语言特征,此子集包含了事件驱动、基于共享变量的并发特性、时间延迟等Verilog的主要语言成分.在此操作语义模型中,所有的Verilog程序将被统一地认为是开放式系统,所以在此操作语义模型的基础上能够进一步提出Verilog开放进程的观察模型,并提出基于互模拟的观察等价概念来判定进程之间的等价关系.最后证明了所定义的观察等价关系对所有的Verilog构造子而言是一个同余关系,从而为发展相应的进程代数理论提供了一个可靠性基础.     

使用延时演算的时间化RSL的指称语义

使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化.     

自动产生一个图书馆的快速原型

AutoPA1.0是一套基于形式化方法的应用程序.它是一个基于需求规范而自动生成软件快速原型的Java代码的软件, 有着坚实、可靠的理论基础.给出一个图书馆管理系统的例子, 阐述如何用UML建立需求模型,然后用AutoPA1.0生成该需求模型对应的软件快速原型的Java代码. 采用的需求模型主要包括一个用况模型和一个概念类模型, 分别用UML中的用况图和类图描述.生成的软件快速原型将包括用况图中每个用例的执行,用一个系统数据库来描述当前系统状态, 该系统数据库保存了当前系统中存在的所有对象以及对象之间的关系.     

Verilog代数语义研究

给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互模拟的.研究了此代数语义的相对完备性,即参照前面的操作语义模型,相对于扩展Verilog语言的一个子集而言,此代数语义是完备的.即所有符合这样语法的程序,如果它们是互模拟等价的,那么它们同样可以在所提出的代数系统中被推导相等.在完备性证明过程中,采用范式方法,即构造一种语法上特殊的程序,任何属于上述子集中的一个程序通过该代数规则都能够被转化为范式程序,而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的.上述结果具有重要的理论意义,因为现有的进程代数理论主要是针对管道通信并行语言而展开的,而对于像Verilog这种以共享变量通信为基础的复杂并行语言研究还是比较少的,对此类复杂的基于共享变量的并行语言的进程代数理论研究提出了一种通用、有效的方法.     

面向OWL知识的问答系统:Agile

在清华大学973汉语树库的基础上,根据汉语词汇的句法功能分布状况,构建了句法功能分布知识库。在构建的句法功能分布知识库基础上,使用CABOSFV(Clustering Algorithm Based On Sparse Feature Vector)聚类算法,从中挖掘了汉语词汇的类别知识,并对这些类别知识逐一进行了分析。     

数字系统中高层次设计的最优调度算法比较

高层次设计技术是数字系统设计的关键技术，是近年来国内外研究、开发和应用的热门课题。文章用形式化方法描述了两种流行的高层次设计的软件算法，并进行了实验验证。