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

2.
李勇坚  孙永强  何积丰 《软件学报》2001,12(10):1573-1580
在连续离散混合时间模型中考虑Verilog的语义行为,将混合模型中的一个区间作为Verilog程序一次运行过程的指称.提出了一种扩展的ITL来描述这种混合区间,从而给出Verilog的形式语义.这种语义定义不仅考虑到了各种语言成分的最终执行结果,而且能够很好地给出语言成分执行的时序特征.  相似文献   

3.
基于操作语义的磁臂隐通道分析*   总被引:1,自引:0,他引:1       下载免费PDF全文
深入分析磁臂隐通道的产生及产生的原因,发现目前基于系统顶级描述和基于系统源代码搜索方法难以找出这类隐通道,提出一种基于操作语义的方法来研究磁臂隐通道,将磁臂调度过程中的进程看做一个抽象机,以Plotkin的结构化操作语义给出电梯调度算法的推导规则;根据推导规则得到进程抽象机所有状态以及进程抽象机状态的动态变化历史,这样就构成完整的信息传导操作语义模型.研究与分析两个高低安全级进程抽象机状态变迁及状态变迁序列,从而找到其中存在的磁臂隐通道.  相似文献   

4.
使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证.  相似文献   

5.
本文利用形式化的方法对SystemVerilog的指称语义进行研究,采用EBES(extended bundle event strueture)作为抽象模型,以便更好的描述SystemvPrilog真并发的特点.我们的主要工作是:首先,通过对SystemVefilog语言的认真学习,从中抽取出一个尽可能多的包含其语法的真并发子集;其次,利用进程代数LOTOS描述其基于EBES模型的指称语义,以提供一个准确的、无二义性的SysteroVerilog文档,避免硬件设计中的逻辑性错误.  相似文献   

6.
移动数据库中基于语义的移动子集的构造与替换   总被引:1,自引:0,他引:1  
本文针对移动数据库中缓存的特殊性,提出了移动子集的概念.移动子集是基于语义的客户机上的缓存;它能够减少移动客户机和服务器间的通讯开销,并能让客户机有更好的自治性,有效地支持客户机的断接操作.本文讨论了基于语义的移动子集的构造及其替换策略.  相似文献   

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

8.
语义分析和结构化语言模型   总被引:3,自引:0,他引:3       下载免费PDF全文
李明琴  李涓子  王作英  陆大? 《软件学报》2005,16(9):1523-1533
提出了一个语义分析集成系统,并在此基础上构建了结构化的语言模型.该语义分析集成系统能够自动分析句子中各个词的词义以及词之间的语义依存关系,达到90.85%的词义标注正确率和75.84%的语义依存结构标注正确率.为了描述语言的结构信息和长距离依存关系,研究并分析了两种基于语义结构的语言模型.最后,在中文语音识别任务上测试两类语言模型的性能.与三元语言模型相比,性能最好的语义结构语言模型--中心词三元模型,使绝对字错误率下降0.8%,相对错误率下降8%.  相似文献   

9.
基于轨迹的程序语义之一:轨迹与语义对象   总被引:2,自引:0,他引:2  
王岩冰  陆汝占 《软件学报》1998,9(5):366-370
本文提出一种基于轨迹的指称语义框架,该框架结合了操作语义和代数语义的特征,避免使用专门的数学理论,将静态语义和动态语义结合在一起统一处理.本文及其续篇将通过一个中等规模的过程式模型语言来说明上述语义框架更适合描述真正的程序设计语言.本文首先引入轨迹概念和模型语言,然后讨论该语言的各句法成分所对应的语义论域,其中没有使用含有函数空间构造运算的递归论域方程.  相似文献   

10.
为了刻画多Agent环境中的交互特性,基于流演算理论和GoFlux语言,吸收了ConGolog语义,提出了CFlux语言。CFlux语言能有效地处理MAS中的For循环、并发、优先级并发、中断等操作,从而可以实现多Agent程序的并发交互执行。在此基础上,基于CFlux和一组通信动作提出一个请求/服务协作模型。最后,通过一个智能日程安排实例表明了上述理论。  相似文献   

11.
12.
袁春  陈意云 《计算机学报》2000,23(8):877-881
针对一个基于共享变量的带有进程创建的命令式语言,用变迁系统描述了它的结构操作语义,并用扩展的状态变迁迹模型定义了它的指称语义,在该模型下,状态变迁被区分为两种不同形式,分别表示发生在原进程和被创建进程中的状态变迁,这样便可以定义适当的语义复合运算,在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接,恰当地反映了进程的并发运行受创建命令在程序中的相对位置的限制,最后证明了这两个语义  相似文献   

13.
14.
A basic question in the theory of communicating processes is “When should two processes be considered equivalent?”. Attempts to answer this question have led to the concepts of observation equivalence, bisimulations, testing equivalence, failure equivalence, etc. The main point of this paper is to increase the understanding and motivation for two of these equivalences, namely failure and testing equivalences. The approach starts with the idea that the equivalence of processes should be reducible to the visible sequences of actions which a process performs in various contexts. This idea is implemented by a string-based semantic order for communicating processes where divergence is catastrophic. Under some assumptions about contexts, the resulting semantics is shown to be equivalent to theimproved failure semantics of Brookes and Roscoe(1) and also to themust testing-semantics of Hennessy and DeNicola.(2–4) This characterization gives independent support for the appropriateness of failures and testing.  相似文献   

15.
This paper investigates the operational semantics of temporal logic programs. To this end, a temporal logic programming language called Framed Tempura is employed. The evaluation rules for both the arithmetic and boolean expressions are defined. The semantic equivalence rules for the reduction of a program within a state is formalized. Furthermore, the transition rules within a state and transition rules over an interval between configurations are also specified. Moreover, some examples are given to illustrate how these rules work. Thus, the executable behavior of framed programs can be captured in an operational way. In addition, the consistency between the operational semantics and the minimal model semantics based on model theory is proved in detail.  相似文献   

16.
《国际计算机数学杂志》2012,89(12):2040-2060
We apply a testing approach to the Calculus of Fair Ambients and investigate the resulting testing equivalence. We prove that variant conditions on its definition do not change its discriminating power, and it is congruent on finite processes. On a proper subset of processes, open bisimilarity is strictly included in testing equivalence. It is also proved that the translation from Pi-Calculus to Fair Ambients is fully abstract with respect to testing equivalence.  相似文献   

17.
In this paper we extend de Nicola and Hennessy’s testing theory to deal with probabilities. We say that two processes are testing equivalent if the probabilities with which they pass any test are equal. We present three alternative semantic views of our testing equivalence. First, we introduce adequate extensions of acceptance sets (inducing an operational characterization) and acceptance trees (inducing a denotational semantics). We also present a sound and complete axiomatization of our testing equivalence. So, this paper represents a complete study of the adaptation of the classical testing theory for probabilistic processes.  相似文献   

18.
A comparative semantic study is made of an element of the family of concurrent object-oriented programming languages. Particular attention is paid to two notions: (i) dynamically evolving process structures, including a mechanism to name and refer to processes and a means to create new processes, and (ii) rendez-vous between processes involving the sending and answering of messages and the induced execution of method calls. The methodology of metric semantics is applied in the design of operational and denotational semantics, as well as in the proof of their equivalence. Both semantics employ domains which are determined as fixed points of a contracting functor in the category of complete metric spaces. Moreover, fruitful use is made of the technique of defining semantic meaning functions as fixed points of contracting higher-order mappings. Finally. syntactic and semantic continuations play a pervasive role.  相似文献   

19.
As the size and efficiency of computers increases, it is clear that they will be used for extremely large file information storage and retrieval banks, in particular for non-scientific documents and data. Such an information bank might be, for example, the legal code for a large country or even the legal codes of all countries. Another example might be individual medical histories for a large population base, possibly the whole world. Storage and retrieval algorithms for such large files present special problems. It is no longer feasible, for instance, for the computer to consider every item in the memory in order to retrieve a designated subset. The problem, then, is how to classify the information, that is, divide it up into disjoint categories so that retrieval is feasible, efficient, and accurate. The present paper presents a general approach or logical framework for handling such problems. The basic observation is that classification really amounts to introducing an equivalence relation on the universal set of all the items in the file. The problem is how to define these equivalence relations in a natural manner, that is, in a manner which reflects something of the structure of the information and which thus allows us to store and retrieve the information in a structured fashion. This classification procedure is not conceived as being an algorithm but rather a mathematical procedure on which various algorithms can be based. This procedure can be described as follows: First a very broad, initial classification is made. For each such classification, there is a standard or canonical form. The canonical form involves some finite number of parameters. Syntactically these parameters are just terms of various sorts, but our approach is to consider rather the universe of values of each parameter. This is the semantic universe associated with the given parameter. These semantic universes are seen to have a very natural structure when they are considered in a certain way as subcollections of a type-theoretic universe based on some concrete set (such as the set of people, the set of married couples, etc). This structure allows us to define the desired equivalence in a natural way on a given semantic universe. Taking the conjunction of the parameters occurring in a given canonical form we thus get a classification for the sentences having that canonical form. Since this obtains for each canonical form, we thus have a classification for the whole information bank. Concrete examples are given to illustrate the applicability of this approach. The approach is, in fact, a mathematical generalization of a concrete case already treated by this method.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号