云南高校图书馆联盟文献共享服务平台- OBJECT-Z

OBJECT-Z: 作品数：40被引量：59H指数：4; 导出分析报告; 相关领域：自动化与计算机技术更多>>; 相关作者：缪淮扣文志诚陈怡海应时江春更多>>; 相关机构：上海大学武汉大学福州大学苏州大学更多>>; 相关期刊：《计算机应用与软件》《计算机应用研究》《小型微型计算机系统》《软件学报》更多>>; 相关基金：国家自然科学基金国家重点基础研究发展计划上海市教育委员会重点学科基金国家高技术研究发展计划更多>>

一种支持设计时软件重用的反射式软件体系结构及其形式化研究被引量：3: 《计算机工程与科学》2019年第8期1434-1443,共10页罗巨波应时刘天时; 陕西省教育厅科研计划项目资助(项目编号:18JK0621);国家自然科学基金(61672392,61373038); 软件体系结构在软件重用中有着特殊的意义。缺乏显式的描述并使用支持体系结构重用过程的信息和缺乏有效的重用方法是软件体系结构难以重用最根本的原因。在软件设计阶段,将元信息、元建模、反射和软件体系结构结合起来,构造了一种支持...; 关键词：软件体系结构重用反射式软件体系结构具体化 Object-Z形式化描述

基于Object-Z生成Python代码的研究被引量：1: 《电子技术与软件工程》2019年第5期234-235,共2页袁鼎刘振宇; (基金编号:2018KYY086)南华大学研究生科研基金支持; 在本文中,我们将提出一种从OZ到Python的映射去验证这些规范。在这个映射中,包括前置条件、后置条件和变量都将被验证,这些都是建立在使用lambda函数(以下简称L函数)和Python的编辑器上的。本研究发现Python对于开发从OZ映射到Python的...; 关键词：OBJECT-Z PYTHON 面向对象编程契约式设计

The high level language for system specification: A model-driven approach to systems engineering被引量：1: 《International Journal of Modeling, Simulation, and Scientific Computing》2016年第1期180-214,共35页Hamzat Olanrewaju Aliyu Oumar Maıga Mamadou Kaba Traore; We present HiLLS(High Level Language for System Specification),a graphical formalism that allows to specify Discrete Event System(DES)models for analysis using methodologies like simulation,formal methods and enactmen...; 关键词：HiLLS modeling and simulation integrated formalism DEVS OBJECT-Z

形式语言Object-Z的模型检测研究: 《苏州市职业大学学报》2015年第3期29-35,共7页吴彩燕; 苏州市职业大学青年基金资助项目(2014SZDQ06); Object-Z是一种用于表示面向对象系统规约的高层抽象语言,由于缺乏自动验证工具的支持,很难建立直接证明由Object-Z表示的面向对象系统规约正确性,成为Object-Z被广泛采用的最大障碍.模型检测是一种验证系统规约正确性的自动化技术.使...; 关键词：模型检测 OBJECT-Z SPIN 时序逻辑

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述被引量：2: 《计算机科学》2014年第4期184-189,共6页马莉钟勇霍颖瑜; 广东省自然科学基金(10152800001000016);佛山市科技发展专项资金(2011AA100061);佛山市产学研专项资金(2012HC10027)资助; Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描...; 关键词：形式化描述语言责任授权模型 OBJECT-Z 分布式时态逻辑

Object-Z规格到实现机制探讨: 《计算机光盘软件与应用》2013年第21期59-61,58,共4页王志刚谢茂芳; 形式化规格是保证所设计的系统具有较高的可信度和正确性的重要途径,它涉及软件生命周期的各个阶段。从形式化规格到软件编码是软件开发中的一个关键环节。在分析了规格化和高级语言之间的内在关系的基础上,概括了基于Object-Z规格到Jav...; 关键词：软件体系结构形式规格 OBJECT-Z JAVA 转换机制

基于MDA的MARTE模型形式化转换被引量：2: 《指挥控制与仿真》2012年第6期128-133,共6页王立杰刘昌禄俞烈彬; 总装备部"十二五"基金项目; 非形式化/半形式化模型到形式化模型之间的转换是当前软件工程领域的研究热点。根据异构模型转换,提出了基于MDA的MARTE模型到Object-Z规约之间的转换方法。针对Object-Z在实时领域表达能力不足的问题,首先扩展Object-Z元模型;然后在MD...; 关键词：模型驱动 MARTE模型 Object-Z规约元模型模型转换

基于Object-Z的Web组件形式化建模被引量：1: 《计算机科学》2012年第B06期383-388,407,共7页严吉皞缪淮扣; 国家自然科学基金项目(60970007);上海市科学技术委员会(10510704900);上海市重点学科建设项目(J50103)资助; Web组件技术是一种解决Web服务再利用和扩展问题的方法。Object-Z是Z语言的面向对象补充,它们是基于一阶谓词逻辑和集合论的形式规格说明语言。用形式规格说明语言Object-Z对Web组件建模,能够保证Web组件在异构平台、松散耦合、封装等...; 关键词：WEB组件组件组合 OBJECT-Z 定理证明

基于Object-Z与Markov链的校园卡系统测试用例: 《微电子学与计算机》2012年第3期73-77,共5页仲晓敏侯建花杨长青; 国家自然科学基金项目(50806011); 针对提高校园卡系统准确性和可靠性测试的要求,提出了Object-Z与Markov链结合的测试用例自动生成算法.使用Object-Z对系统进行形式化规约,生成测试场景和操作顺序图;将操作顺序图转换为Markov链使用模型;根据测试场景和Markov链使用模...; 关键词：校园卡系统 OBJECT-Z 测试场景 MARKOV链使用模型测试用例

Object-Z规格说明测试用例的自动生成器被引量：5: 《软件学报》2011年第6期1155-1168,共14页许庆国缪淮扣曹晓夏胡晓波; 国家自然科学基金(60970007;61073050);国家重点基础研究发展计划(973)(2007CB310800);上海市自然科学基金(09ZR1412100);上海市科学技术委员会项目(10510704900);上海市重点学科建设项目(J50103);武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-26); 对Object-Z形式规格说明构造测试用例的研究,目前主要集中在理论研究阶段,测试用例的自动生成几乎没有相应的工具支持.Object-Z是基于数学和逻辑的语言,并大量使用了模式复合和简写形式,这给计算机提取完整语义用以自动产生测试用例造...; 关键词：基于规格说明的测试 OBJECT-Z 语义提取测试用例生成器

OBJECT-Z