V8.0 版权所有© 2001-2026 渝B2-20050021-1
渝公网安备 50019002500403号违法和不良信息举报中心举报邮箱：jubao@cqvip.com
互联网出版许可证 新出网证(渝)字10号机构客服热线 023-67882612
- Object-Z规格说明测试用例的自动生成器 认领 引用 被引量：5
- 1
- 《软件学报》 EI CSCD 北大核心 2011年第6期1155-1168,共14页
- 对Object-Z形式规格说明构造测试用例的研究,目前主要集中在理论研究阶段,测试用例的自动生成几乎没有相应的工具支持.Object-Z是基于数学和逻辑的语言,并大量使用了模式复合和简写形式,这给计算机提取完整语义用以自动产生测试用例造... 展开更多
- 关键词 基于规格说明的测试 Object-Z 语义提取 测试用例生成器
- 基于Object-Z的形式化验证方法 认领 引用 被引量：7
- 2
- 《计算机科学》 北大核心 2007年第5期247-251,共5页
- 定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,... 展开更多
- 关键词 Object-Z 形式化验证 前后置条件 状态空间 电梯操作系统
- DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述 认领 引用 被引量：2
- 3
- 《计算机科学》 CSCD 北大核心 2014年第4期184-189,共6页
- Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描... 展开更多
- 关键词 形式化描述语言 责任授权模型 Object-Z 分布式时态逻辑
- 一种基于Object-Z的面向方面建模方法 认领 引用 被引量：1
- 4
- 《华东理工大学学报（自然科学版）》 EI CAS 北大核心 2007年第3期383-388,共6页
- 提出一种基于Object-Z的形式化面向方面建模语言及其建模方法。方面规范提供了观察基本模块和方面模块的行为、描述它们相互关系的手段,编织机制将两类模块系统地集成为一个完整的系统模型。该方法能有效地简化系统建模,提高系统模型的... 展开更多
- 关键词 面向方面 形式化方法 Object-Z 建模
- 用UML和Object-Z描述交互式系统的接口规格说明 认领 引用 被引量：3
- 5
- 《小型微型计算机系统》 EI 北大核心 2002年第10期1169-1172,共4页
- 随着图形用户界面的普及 ,交互已成为目前软件系统的一个重要特征 .与传统的基于字符界面的软件系统相比 ,基于图形用户界面的软件系统 ,从某种程度上可看作是一个交互式系统 .形式化的规格说明具有精确性、无二义性和一致性等优点 ,用... 展开更多
- 关键词 UML Object-Z 描述交互式系统 接口规格说明 软件工程 用户接口 对象建模语言 形式化说明语言
- 基于Object-Z多态推理 认领 引用 被引量：2
- 6
- 《计算机科学》 北大核心 2006年第7期230-232,256,共3页
- Object-Z是形式规格说明语言Z的面向对象扩充,基于严格的集合论与数理逻辑,具有面向对象的特点:类、对象、继承、封装与多态等。用它可以精确描述大型软件需求规格说明,且能够进行严密的逻辑推理与验证。本文主要探讨了它的多态性推理,... 展开更多
- 关键词 Object-Z 多态 前置条件 后置条件 推理 重用
- 带OCL约束条件的类图到Object-Z规格说明的转换 认领 引用 被引量：4
- 7
- 《计算机科学》 北大核心 2007年第1期228-235,共8页
- 如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的... 展开更多
- 关键词 UML 类图 OCL约束 Object-Z规格说明
- OCL与Object-Z作为UML约束语言的分析比较 认领 引用 被引量：4
- 8
- 《计算机科学》 北大核心 2004年第12期182-185,共4页
- UML是目前广泛使用的标准的面向对象建模语言。为了提高建模的精确性,UML模型可以用对象约束语言OCL或者是用Object-Z规格说明语言加以补充说明。本文从多个方面分析比较了这两种语言的特点,并提出建模人员应充分利用这两种语言的特点,... 展开更多
- 关键词 Object-Z UML模型 OCL 面向对象建模语言 对象约束语言 规格说明 系统 分析比较 人员 标准
- 用带时钟变量的线性时态逻辑扩充Object-Z 认领 引用 被引量：1
- 9
- 《计算机应用研究》 北大核心 2009年第5期1764-1769,共6页
- Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首... 展开更多
- 关键词 Object-Z 用带时钟变量的时态逻辑 实时系统 形式规格说明 形式验证
- 一个Object-Z规格说明的证明责任产生器 认领 引用 被引量：1
- 10
- 《计算机应用与软件》 2010年第5期34-37,共4页
- 定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,... 展开更多
- 关键词 Object-Z Z/EVES 证明责任 形式验证
- 使用Object-Z获取形式需求 认领 引用 被引量：1
- 11
- 《计算机辅助工程》 2008年第1期87-90,共4页
- 针对软件需求描述中用UML描述的模型与形式需求说明相比不利于推理和验证的问题,使用统一过程建立用UML描述的需求模型并对其进行形式化,获得用Object-Z描述形式需求说明的方法和步骤,并结合实例进行论述.提出利用形式方法验证和确认非... 展开更多
- 关键词 统一过程 UML 形式方法 Object-Z
- 基于Object-Z与Markov链的校园卡系统测试用例 认领 引用
- 12
- 《微电子学与计算机》 CSCD 北大核心 2012年第3期73-77,共5页
- 针对提高校园卡系统准确性和可靠性测试的要求,提出了Object-Z与Markov链结合的测试用例自动生成算法.使用Object-Z对系统进行形式化规约,生成测试场景和操作顺序图;将操作顺序图转换为Markov链使用模型;根据测试场景和Markov链使用模... 展开更多
- 关键词 校园卡系统 Object-Z 测试场景 Markov链 使用模型 测试用例
- Object-Z规格到实现机制探讨 认领 引用
- 13
- 《计算机光盘软件与应用》 2013年第21期59-61,58,共3页
- 形式化规格是保证所设计的系统具有较高的可信度和正确性的重要途径,它涉及软件生命周期的各个阶段。从形式化规格到软件编码是软件开发中的一个关键环节。在分析了规格化和高级语言之间的内在关系的基础上,概括了基于Object-Z规格到Jav... 展开更多
- 关键词 软件体系结构 形式规格 Object-Z Java 转换机制
- 基于Real-Time Object-Z语言的铁路交叉道口系统的形式化描述 认领 引用
- 14
- 《郑州轻工业学院学报（自然科学版）》 2009年第3期32-36,共5页
- 形式化语言Object-Z的实时扩展Real-Time Object-Z可以对实时系统进行形式化描述.以铁路交叉道口系统的应用证明了这一点.
- 关键词 Real-Time Object-Z 铁路交叉道口系统 形式化描述
- Object-Z规格说明的结构模拟动画技术 认领 引用 被引量：4
- 15
- 《上海大学学报（自然科学版）》 CAS 北大核心 2005年第6期589-595,共7页
- 形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一... 展开更多
- 关键词 形式方法 形式规格说明 确认 动画模拟 Object-Z Prolog SICStus Prolog
- 基于Object-Z的XPath形式化语义 认领 引用 被引量：1
- 16
- 《计算机科学》 北大核心 2004年第2期175-180,共6页
- 本文描述了XPath语言的形式化语义。一个统一的面向对象的语义视角用于建模所有XPath语言构造。语义的表示采用形式化规范语言Object-Z的符号系统。这种高度结构化的语义模型具有简洁、可组合性和可复用性的特点。
- 关键词 XPath语言 形式化语义 Object-Z 面向对象 数据类型 程序设计语言
- 基于Object-Z的UML对象模型的形式化 认领 引用 被引量：1
- 17
- 《计算机科学》 北大核心 2000年第2期60-63,共4页
- 1 引言 UML作为面向对象的可视化建模语言,己被对象管理集团(OMG)作为面向对象分析和设计的标准,获得了众多工具的支持。UML提供了不同抽象层次的描述以支持面向对象的分析、设计和实施,它从不同的视图描述软件系统,减少了建模的复杂度... 展开更多
- 关键词 UML语言 面向对象 Object-Z 对象模型
- 基于Real-Time Object-Z语言的实时系统形式化描述 认领 引用 被引量：2
- 18
- 《重庆师范大学学报（自然科学版）》 CAS 2007年第4期41-44,53,共4页
- 实时系统是一类需要考虑时间约束条件的反应系统,确保实时系统安全性和可靠性是至关重要的。形式化方法是建立在严密数学基础之上的开发方法,采用形式化方法对实时系统进行描述与验证,可以借助严密的数学证明提高实时系统的安全性和可... 展开更多
- 关键词 实时系统 Object-Z Real-Time Object-Z 实时精化演算 形式化描述
- 基于Object-Z的带OCL约束的UML类图形式化描述 认领 引用 被引量：1
- 19
- 《沈阳师范大学学报（自然科学版）》 CAS 2008年第4期456-459,共4页
- UML OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行约束后类图便具备严格语法和精确语义,同时也具备了演绎验证的基本条件;但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证.因此提出了一种带OCL... 展开更多
- 关键词 统一建模2.0 对象约束语言 形式化语言Object-Z
- 基于Object-Z生成Python代码的研究 认领 引用 被引量：1
- 20
- 《电子技术与软件工程》 2019年第5期234-235,共2页
- 在本文中,我们将提出一种从OZ到Python的映射去验证这些规范。在这个映射中,包括前置条件、后置条件和变量都将被验证,这些都是建立在使用lambda函数(以下简称L函数)和Python的编辑器上的。本研究发现Python对于开发从OZ映射到Python的... 展开更多
- 关键词 Object-Z Python 面向对象编程 契约式设计
