陈怡海

作品数：16被引量：28H指数：4
导出分析报告
供职机构：上海大学计算机工程与科学学院更多>>
发文主题：UML软件开发OBJECT-Z动画模拟定理证明更多>>
发文领域：自动化与计算机技术文化科学社会学经济管理更多>>
发文期刊：《计算机工程》《中国信息技术教育》《信息技术与标准化》《福建电脑》更多>>
所获基金：国家自然科学基金国家重点基础研究发展计划上海市教育委员会重点学科基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
以软硬件协同开发为向导的本科创新实践课程探索
《中国教育信息化》2021年第11期82-85,共4页高洪皓 陈章进 陈怡海 王镜杰 
2018年全国高等院校计算机基础教育研究会计算机基础教学改革课题(编号:2018-AFCEC-309);谷歌信息技术(中国)有限公司&教育部高等教育司关于公布2019年第二批产学合作协同育人项目资助。
程序设计课程以教为主,创新实践课以实操为主。文章以“搭建智能小车和控制系统”为创新实践需求,充分利用课上和课下资源,促使本科生将程序设计、机械自动化、通信等多学科知识点进行融合,强化基础课程和实现培养独立创新能力;将程序...
关键词：软硬件协同开发 程序设计与多学科交叉 创新实践 智能小车和控制系统 
日常教学数据分析与可视化方法——以“程序设计方法学”课程为例被引量：2
《中国信息技术教育》2018年第21期99-102,共4页刘悦 蔡飞 陈怡海 王皙 张博锋 
上海高校外国留学生英语授课示范性课程建设项目(软件工程)(上海市教育委员会文件教外[2016]83号);上海市教委重点课程建设项目(程序设计方法学)(上海市教育委员会文件沪教委高[2015]37号))共同资助
本文分析了课程建设网站采集的日常教学数据的类型和特点,并针对这些数据,采用统计分析和Echarts技术,以可视化的形式展现了师生的日常教学情况,分析了其与教学效果的关联关系,进而,提出了基于回归的学生成绩绩点预测方法,综合考虑了学...
关键词：教学数据分析 可视化 回归 
基于Python的Moodle平台数据可视化被引量：2
《福建电脑》2018年第9期27-28,共2页陈怡海 韦岚 刘悦 
上海高校外国留学生英语授课示范性课程建设项目(软件工程)(上海市教育委员会文件教外[2016]83号);上海市教委重点课程建设项目(程序设计方法学)(上海市教育委员会文件沪教委高[2015]37号))共同资助
Moodle是一个广泛使用开源的课程管理系统,对Moodle学习数据进行数据分析和可视化是教师不可或缺的重要手段和工具。本文以Python作为编程开发语言,选用My SQL数据库作为后台数据库,对Moodle平台的访问数据进行分析研究,设计实现了一个M...
关键词：MOODLE 学习管理系统 数据可视化 PYTHON 
新版软件产品质量要求和测试标准剖析被引量：3
《信息技术与标准化》2015年第4期42-45,共4页胡芸 陈怡海 
介绍了新版软件产品质量要求和测试标准ISO/IEC 25051:2014的制定背景及其与ISO/IEC 25051:2006的内容对比,具体阐述了二者在适用范围、软件质量特性、标准内容等方面的差异,从而有利于测评人员更好的理解与使用该标准。
关键词：ISO/IEC 25051 软件产品 测评 剖析 
表格语言的分析比较
《计算机科学》2014年第3期23-26,共4页陈怡海 缪淮扣 
国家自然科学基金项目(61073050;61170044)资助
表格语言具有可读性和可理解性的优点,它能非常精确地表示软件系统需求。在过去的30多年间,表格语言已经成功地应用于多个安全关键嵌入式软件的开发中。准确了解这些表格语言的特性,对表格语言的研究及推广有重要的指导意义。对3种不同...
关键词：表格方法 形式方法 规格说明验证与确认 工具支持 
流媒体技术在证券股评系统中的应用研究
《计算机工程》2008年第3期253-255,共3页黄铁山 吴绍春 陈怡海 
流媒体技术是在数据网络上以数据流的方式传输多媒体信息的技术,被认为是未来高速网络的主流应用之一。该文研究流媒体关键技术中的音视频数据采集和编码技术,解决在多媒体数据应用平台中双数据流的同步和传输问题。综合应用到某证券公...
关键词：流媒体 数据流压缩/编码 双流同步和传输 
定理证明辅助工具Isabelle剖析与应用
《计算机应用与软件》2007年第8期14-16,43,共4页郭慧梅 缪淮扣 陈怡海 
国家自然科学基金项目(60373072;60673115);上海市教委科技发展基金(05AZ70)。
Isabelle是一个通用的定理证明器,应用领域广泛。介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法。
关键词：逻辑系统 定理证明器 形式化方法 
带OCL约束条件的类图到Object-Z规格说明的转换被引量：4
《计算机科学》2007年第1期228-235,共8页缪淮扣 陈怡海 
国家自然科学基金(项目编号60373072);国家973项目(批准号2002CB312001);上海市教委第四期重点学科建设基金的资助
如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的...
关键词：UML 类图 OCL约束 OBJECT-Z规格说明 
Object-Z规格说明的结构模拟动画技术被引量：4
《上海大学学报（自然科学版）》2005年第6期589-595,共7页朱江 陈怡海 缪淮扣 
国家自然科学基金资助项目(60373072);上海市教委科学技术发展基金资助项目(02AK07)
形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一...
关键词：形式方法 形式规格说明 确认 动画模拟 OBJECT-Z PROLOG SICStus PROLOG 
一个Z的证明责任产生器被引量：2
《上海大学学报（自然科学版）》2005年第5期495-499,共5页沈毅 缪淮扣 文志诚 陈怡海 
国家自然科学基金资助项目(60373072);上海第四期重点学科建设资助项目
在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明...
关键词：形式规格说明 验证 Z 证明责任 前置条件 不变式 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部