Verilog代数语义研究

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

Verilog语言形式化语义研究

在连续离散混合时间模型中考虑Verilog的语义行为,将混合模型中的一个区间作为Verilog程序一次运行过程的指称.提出了一种扩展的ITL来描述这种混合区间,从而给出Verilog的形式语义.这种语义定义不仅考虑到了各种语言成分的最终执行结果,而且能够很好地给出语言成分执行的时序特征.     

Verilog语义的ASM表示方法研究

使用抽象状态机模型（ASM）对Verilog的语义进行研究,给出各类赋值语句和延迟/事件控制结构的形式定义。以此为基础与VHDL进行对比,说明各种赋值语句和延迟/事件控制结构向VHDL的转换方法以及二者在转换前后的差异。     

支持并行模拟的Verilog编译技术研究与实现

并行HDL模拟是加速大型复杂的VLSI系统模拟验证的有效方法,支持并行模拟的HDL编译技术是其中的关键技术,文章提出了一种支持并行模拟的Verilog编译技术,编译器将Verilog描述转换成C＋＋代码,最后与并行模拟核心库编译链接生成可执行并行程序。文章将编译器构成,代码生成方法和并行模拟核心库,该技术已经在并行Verilog模拟器ParaVer上实现。     

语义特征建模系统中操作局部化的研究

为了提高语义特征建模系统约束求解的效率及系统的整体性能,提出了一种新的操作局部化方法。该方法使用特征语义表示法来描述产品模型中特征的各种信息,改进了细胞元模型对特征元素的管理机制,通过特征的“语义面”将局部特征从模型中有效地分离出来,通过创建临时特征的方法来实现模型的局部约束求解。该策略不仅可以完全满足在复杂模型中直接操作的需要,还可以大大提高系统的性能。实验表明该算法具有更强的适应性和实用性。     

基于逻辑的软件演化操作语言及结构化操作语义

由于使用环境和新技术的不断变化,软件演化的控制变得日趋复杂.为了提高软件演化活动的可视化和形式化支持程度,结合谓词逻辑和软件演化,提出了一种软件演化操作语言SEOL(Software Evolution Operational Language)描述软件演化,给出了SEOL的语法和结构化操作语义描述,并指出了软件演化操作语义等价分析方法.结合软件代码演化和软件模型演化实例,说明了SEOL的应用.与已有的软件演化操作描述相比,SEOL在易用性、可重用性和形式化分析方面有明显的改善,为软件演化的管理、分析和实施奠定了基础.     

UML顺序图的结构化操作语义研究

UML顺序图侧重于展示对象之间的消息交互过程,但其动态语义缺乏形式化的描述,不利于对顺序图模型的准确理解和基于该模型的测试用例生成。为此,依据UML1. 5规范,采用BN定义顺序图的形式化语法,提出了活动点的概念;在此基础上,讨论并给出了单个对象执行消息动作的结构化操作语义以及顺序图模型的整体结构化操作语义,为模型检验和基于顺序图的测试用例生成提供了前提。     

协同CAD系统中操作语义共享技术研究

研究了协同CAD系统的操作语义,给出了操作语义的定义和描述方法、操作语义的识别技术以及基于本体的映射模型,在此基础上提出了一种基于操作语义共享的CAD协同框架,最后给出了基于该框架的一个原型系统。     

rCOS的操作语义在程序分析中的应用研究

本文给出了rCOS语言的一种操作语义。并说明该操作语义在程序分析中的一个应用,即模式识别。为了能够判断在以rCOS为元语言编写的程序中,是否正确地运行了某种设计模式,从而进一步能自动识别出程序中好的模式和坏的模式。     

A Congruence Format for Name-passing Calculi

We define and use a SOS-based framework to specify the transition systems of calculi with name-passing properties. This setting uses proof-theoretic tools to take care of some of the difficulties specific to name-binding and make them easier to handle in proofs. The contribution of this paper is the presentation of a format that ensures that open bisimilarity is a congruence for calculi specified within this framework, extending the well-known tyft/tyxt format to the case of name-binding and name-passing. We apply this result to the π-calculus in both its late and early semantics.     

Branching Bisimulation Congruence for Probabilistic Systems

The notion of branching bisimulation for the alternating model of probabilistic systems is not a congruence with respect to parallel composition. In this paper we first define another branching bisimulation in the more general model allowing consecutive probabilistic transitions, and we prove that it is compatible with parallel composition. We then show that our bisimulation is actually the coarsest congruence relation included in the existing branching bisimulation when restricted to the alternating model.     

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型,该模型由Hennessy和Lin首先提出,随后又被Lin推广至带赋值的符号迁移图,本文不但定义了符号迁移图各种版本（基／符号）的强操作语义和强互模拟,提出了相互的强互模拟算法,而且通过引入符号观察图和符号同余图,给出了其弱互模拟等价和观察同余的验证算法,给出并证明了了τ－循环和τ－边消去定理,在应用任何弱互模拟观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简。     

混合语义时间Petri网的特征条件及时间性质

针对时间Petri网现有强、弱语义模型在调度分析上存在的缺陷以及凝练调度一致性问题和调度时限性问题,提出混合语义模型解决方案,并给出混合语义模型的特征条件,比较混合语义模型与强、弱语义模型的时间互模拟能力,证明混合语义模型的正确性和时间行为的不可替代性。     

Verilog-VHDL翻译器设计与实现

在对Verilog和VHDL两种语言进行全面分析比较的基础上,依据统一的模拟时序模型和设计引用层次,采用模拟语义制导的方法完成从Verilog描述向VHDL描述的翻译转换．在保持功能等价和可综合性的同时,减少对语法和描述风格的限制．最后给出一些典型翻译实例．     

Coalgebra morphisms subsume open maps

We relate two abstract notions of bisimulation, induced by open maps and by coalgebra morphisms, respectively. We show that open maps correspond to coalgebra morphisms for a suitable chosen endofunctor in a category of many sorted sets. This demonstrates that the notion of open-maps bisimilarity is of essentially coalgebraic nature. A central role in our development is played by a category of presheaves, which we show as corresponding to the subcategory of consistent coalgebras with lax cohomomorphisms.     

类型化π演算的双代数语义

证明互模拟同余通常冗长且易出错.双代数为解决该问题提供统一的框架:若行为函子保持弱回拉,共代数范畴到基范畴的忘却函子有右伴函子,则最大共代数互模拟同余.但已有双代数理论建模类型化π演算存在以下困难:行为函子不保持弱回拉,进程互模拟与共代数互模拟不一致.为解决以上两个问题,用稠密拓扑导出布尔范畴作为语义范畴,令行为函子保持弱回拉;定义一类行为函子,使最大进程互模拟与最大共代数互模拟一致,而迟语义和早语义对应的行为函子属于该类函子.进而给出π演算最大进程互模拟同余的双代数模型,为进一步应用双代数框架对其他复杂演算建模奠定了理论基础.