基于Object-Z的带OCL约束的UML类图形式化描述

UML OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行约束后类图便具备严格语法和精确语义,同时也具备了演绎验证的基本条件;但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证.因此提出了一种带OCL约束的UML类图通过Object-Z进行形式化描述的方法,这样便可以充分利用Object-Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等.     

UML 2.0的形式化语义研究

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

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

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

UML状态图的形式化

为面向对象模型建立坚实的形式化基础是近年来形式化研究的热点，UML是一种被推荐的面向对象建模语言，Z是一种广泛使用的形式化规约语言．适合用来精确表示模型的语法和语义，本文利用DFA描述了UML状态机的语法，并采用Z(Object—Z)语言对UML状态机视图进行了形式化描述．     

基于进程代数WS-CDL交互模式建模研究

基于WS-CDL的编排是从全局视角描述Web服务交互功能,但其缺乏形式化语义。基于进程代数提出了PA4WS(Process Algebra for WS-CDL)来描述WS-CDL的形式化语法和语义。相比其他相关工作,PA4WS给出了WS-CDL编排的工作单元建模、基于信息对齐交互模式和异步交互建模。最后,通过一个例子给出了PA4WS带来的好处。     

UML状态机视图的RSL形式描述

使用RAISE规范语言RSL给出了UML状态机视图的形式描述.通过这一形式化提出了一种对图形化的UML状态机视图模型的形式化和RSL规范进行集成的框架,这一工作是对UML类图在RSL中形式化的继续,使得人们可以对UML的非形式化模型给出一种精确、无二义性的语义解释,同时也提高了RSL规范的抽象层次,增强了其可读性、简明性.最后通过一个应用实例,说明这一框架如何用于从UML模型创建对应的形式化规范,并对模型的性质进行了分析.     

一种Verilog的操作语义

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

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

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

RDFS表示本体建模语言OIL的一种方法

给出扩充RDF Schema使之能够表达完全的知识表示语言的方法. 通过为这种语言增加必要的表达能力和语义来完善RDF Schema, 使RDF Schema能够描述本体建模语言OIL. 进一步给出OIL原语的RDF Schema定义： 任何OIL本体都可以使用RDF语法表示, 从而使其具有OIL的推理支持和形式化语义. 这种扩充方法同样也适用于其他知识表示的形式化.     

新闻文本中事件语义表示

事件是比"概念"粒度更大的知识表示单元,更符合人类的认识过程.事件作为新闻文本的知识单元,结合新戴维森事件语义和6要素事件模型,给出了一个新的事件形式化表示方法;扩展不同的操作算子给出了修饰事件要素的模糊信息、对象、时态与环境的形式化表示方法;使用描述逻辑方法描述了事件对象要素中的概念,给出了新闻文本中事件关系形式化的表示方法.实例表明,该方法能够较好地表示新闻文本中的事件语义.     

基于语义和结构的UML类图的检索

以软件重用为背景提出基于语义和结构的UML类图检索.构建了UML类图的重用模型,定义了存储UML类图的重用库结构.提出将本体的概念语义距离应用到UML类图的语义相似性度量和使用图表示UML类图的结构进行结构相似性度量.基于检索流程形式化检索需求,提出了UML类图的检索算法.基于提出的衡量标准,从语义、结构和混合三种检索类型对提出的算法进行了验证.实验结果表明,所提出的检索算法在检索质量和检索效率上要优于其他方法.     

UML 2．0状态图的XYZ/E时序逻辑语义研究

UML2.0状态图适合于描述软件体系结构中组件内部的动态行为及组件端口的行为,但UML2.0状态图的语义不够精确,使得它的描述结果不利于进行进一步的分析和验证。基于此,本文在定义UML 2.0状态图的语法的基础上,给出了UML 2.0状态图的XYZ/E时序逻辑语义,为使用UML 2.0状态图与XYZ/E相结合的方式来描述软件体系结构中组件内部的动态行为及组件端口的行为奠定了基础。     

语义场中同义词竞争的句法优选原则

同一语义场中的同义词存在竞争关系,一般认为语义繁富的词汇往往被替代。＂咀嚼＂义语义场和程度副词语义场中同义词的替代情况表明,相对于语义,句法是个词汇替换的优先原则。     

UML图转有色Petri网图文法

为解决由于UML(Unified Modeling Language)缺少精准的语义表达,使其在系统建模过程中不能给出形式化的验证和分析的问题,提出了UML模型转Petri网模型的图文法,利用Petri网的分析验证技术,实现了对UML模型的正确性验证.在设计阶段即发现系统的缺陷,从而减少软件开发后期发现设计的错误而带来...     

江苏邳州话中的特色否定副词

邳州话的否定副词与普通话的否定副词同中有异。从语义特征和句法分布等方面进行分析,与普通话进行比较研究了邳州话中的两类否定副词：一类是普通话中没有的特色否定副词;一类为普通话中有,但在句法、语义或语用功能上有区别的否定副词。     

英语中名词的可数性

可数性除了指被计数的可能性外,还可以指可数语义或用法,以及可数名词。可数名词就是那些最基本语义为可数用法的名词,并且在这个语义下可以被枚举和复数化。可数性与复数性分属语义和句法领域,且没有一一对应的关系。结合语义和句法两根轴线,英语中的名词可以分成四组,其中可数名词一组,不可数名词三组。一些传统意义上的可数名词如clothes,scissors。cattle,audience等被重新划分为不可数名词。     

“依然”与“仍然”的比较分析

本文在大规模语料的基础上,比较分析现代汉语副词"依然"与"仍然"在句法特征、句式语义和固定格式上的差异。通过分析认为:在句法上,两者都能做状语,而"依然"还可以做谓语;做状语时在大多数情况下两者可以替换。在语义和格式上,"依然"侧重于对静态持续态的修饰,有成词的固定格式;"仍然"可以表动作的间隔重复,并具有更重的转折意味。