国家重点基础研究发展计划(2002CB312001)

作品数：26被引量：149H指数：7
导出分析报告
相关作者：李宣东郑国梁缪淮扣赵建华王林章更多>>
相关机构：南京大学上海大学华东师范大学计算机软件新技术国家重点实验室更多>>
相关期刊：《计算机研究与发展》《计算机工程》《上海大学学报（自然科学版）》《应用科学学报》更多>>
相关主题：UMLMDAEDOC测试用例生成接口自动机更多>>
相关领域：自动化与计算机技术机械工程理学电子电信更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
从集合表达式产生测试数据的方法被引量：3
《计算机工程与设计》2008年第20期5237-5242,共6页胡晓波 缪淮扣 
国家自然科学基金项目(60673115);国家973重点基础研究发展计划基金项目(2002CB312001)
软件测试保证和提高了软件质量,因此成为软件界最为关心的问题之一。测试数据的好坏直接影响软件测试的效果。形式规格说明中的前置条件可用来产生测试数据。而前置条件是基于关系操作符的谓词表达式。给出了一个针对集合关系表达式的...
关键词：形式方法 OBJECT-Z 软件测试 测试数据 集合表达式 代码变异错误测试 
J2EE平台上的所见即所得的HTML电子表格工具的设计被引量：1
《计算机科学》2007年第12期291-293,共3页肖舒 赵建华 李宣东 郑国梁 
国家自然科学基金(批准号60203009;60233020);江苏省自然科学基金(批准号BK2003408);国家973项目(批准号2002CB312001)的资助
本文介绍了一个MDA软件开发工具的设计思想和实现工具。该工具可以根据MDA中的平台无关模型的信息,由用户通过所见即所得的方式来编辑HTML表格。用户编辑了HTML表格框架后,可以基于PIM中的ER模型来定义表格中各个单元格的值。用户在编...
关键词：MDA J2EE 模型转换 表示层 
UML状态图测试充分性准则的公理化评估被引量：8
《上海大学学报（自然科学版）》2007年第5期489-496,共8页缪淮扣 费立志 
国家自然科学基金资助项目(60673115);国家重点基础研究发展计划(973计划)资助项目(2002CB312001);上海市教委科技发展基金资助项目(05AZ70);上海市教委科研项目(07ZZ06)
描述了基于UML状态图测试的一组测试准则,并提出2个新的准则:N-迁移覆盖准则和循环分类覆盖准则.然后提出针对该组测试准则的公理系统,通过此公理系统来评估该组测试准则,给出评估结果.最后根据评估结果得出一些有益的结论.测试准则的...
关键词：UML状态图 测试准则 测试用例 公理化评估 
一种运用模式将CIM转换到PIM的方法被引量：3
《计算机科学》2007年第6期265-269,共5页曹晓夏 缪淮扣 孙军梅 
国家自然科学基金项目(批准号601730301);国家973项目(编号:2002CB312001)资助。
模型转换在MDA软件开发方法中扮演着非常重要的角色,尤其是从CIM到PIM的转换。本文给出了一种从CIM转换到PIM的方法。在CIM中,我们通过特征模型来组织需求,同时用软件体系结构来组织PIM中的各个要素。这个转换中的核心内容是模式的应用...
关键词：MDA CIM PIM 特征模型 模式 责任 
一种动态消减时间自动机可达性搜索空间的方法被引量：1
《计算机科学》2007年第1期213-218,共6页陈铭松 赵建华 李宣东 郑国梁 
国家自然科学基金(No60573085);国家重点基础研究973计划(No2002CB312001)的资助
时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成,时间区域用形如x-y≤(<)n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中,分析算法将生成大量的符号状态,往往...
关键词：时间自动机 模型检验 符号状态 时间区域 
带OCL约束条件的类图到Object-Z规格说明的转换被引量：4
《计算机科学》2007年第1期228-235,共8页缪淮扣 陈怡海 
国家自然科学基金(项目编号60373072);国家973项目(批准号2002CB312001);上海市教委第四期重点学科建设基金的资助
如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的...
关键词：UML 类图 OCL约束 OBJECT-Z规格说明 
基于PVS的时序逻辑语义模型及其实现
《应用科学学报》2006年第6期598-603,共6页许庆国 缪淮扣 
国家自然科学基金(60173031);国家"973"重点基础研究发展计划(2002CB312001)资助项目
时序逻辑作为一种规格说明语言,能够很好地描述程序性质.为了能够利用现有的定理证明器PVS(prototype verification system)对用时序逻辑公式描述的程序性质予以证明,从而达到程序验证的目的.文中在PVS中建立了时序逻辑的语义模型,同时...
关键词：时序逻辑 语义 定理证明 程序性质 
实时系统形式规格说明在PVS中的建立被引量：1
《计算机科学》2006年第12期238-242,共5页许庆国 缪淮扣 
国家自然科学基金项目(批准号60173031);国家973项目(编号:2002CB312001)资助。
本文首先简介了时间自动机和时间B櫣chi自动机形式模型,结合时间化时序逻辑(TimedTemporalLogic)的语法和语义,利用定理证明器PVS(PrototypeVerificationSystem)实现了定义在时间自动机状态(或运行)上的时间化分支(或线性)时序逻辑规格...
关键词：实时系统 时间Büchi自动机 时间化时序逻辑 PVS 
面向服务架构中服务实现的策略被引量：4
《中国科学（E辑）》2006年第10期1220-1239,共20页刘静 何积丰 Zhiming Liu 
国家重点基础研究发展计划(批准号:2002CB312001;2005CB321904);国家自然科学基金(批准号:60373032);上海市自然科学基金(批准号:05ZR14052);教育部211项目资助
构造了层次化的SOA模型,并提出了将服务使用层与服务实现层分层处理的策略.建立了基于服务的构件模型来实现SOA中的服务,使用接口来描述服务的语法,契约来描述服务的语义,并用卫式设计来模服务的行为.将接口作为结合构件技术与面向服务...
关键词：面向服务 接口 契约 构件 
面向服务的软件体系结构的形式化被引量：1
《计算机工程》2006年第8期4-5,共2页孙军梅 缪淮扣 文志诚 
国家"973"计划基金资助项目(2002CB312001);国家自然科学基金资助项目(60373072)
用形式规格说明语言Z对面向服务这样一种新出现的分布式软件体系结构进行形式化,克服了原先面向服务体系结构的非形式化描述中的限制,为更好地进行面向服务的分布式软件开发提供了指导模型。
关键词：软件体系结构风格 面向服务的体系结构 形式化 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部