从计算机工程教育看知识、能力与工程方法浅谈.ppt

实时安全关键操作系统构建和形式验证（续） 结构综合 系统调用 中断处理 例外处理 组件综合 分区管理 进程管理 分区内通信 分区间通信 内存管理 时间管理 文件管理 设备管理 高可信编译系统构建和形式验证 目标：构建支持RISC64位多核CPU，满足MISRA规范的C语言编译系统，并证明语法成分语义与机器代码执行语义等价性。 技术路线图： C语言语法成分对应下推自动机模型。 基于语境，即全局变量和局部变量集合，检查程序的语法结构满足MISRA规范。 给出程序的语法成分语义的等价机器码序列。 形式验证程序的语法成分语义与机器代码执行语义等价，实现高安全性。 高可信编译系统构建和形式验证（续） 结构综合 基于语境的下推自动机 组件综合 语句成份 include 变量定义 主函数及函数 表达式（逻辑、关系及算术） 赋值语句 条件语句 循环语句 符合认证审定的开发环境构建和形式验证 目标：构建符合认证审定的开发环境。 技术路线图： 针对多安全等级的大规模复杂软件的架构建模及形式验证问题，基于功能性、实时性、安全性以及必威体育官网网址性的系统需求 基于领域知识的感知概念与作动概念的因果性关系机理，领域知识子图表征方法及其任务概念模型，发现任务并发机制 基于架构的任务结构与任务功能独立性，以及软件架构代码与软件功能代码分离性质，分别构建软件架构代码和软件功能代码。 面向分区操作系统的基于代换的软件架构代码生成方法，以支持生成满足并发性的大规模复杂软件架构代码 符合认证审定的开发环境构建和形式验证（续） 语境代换公理 并置公理： 赋值公理 条件公理 循环公理 ? 建模工具 领域知识图的构建 高层需求与底层需求形式建模 任务交互行为、功能及程序结构建模 验证与确认工具 形式验证:正确性、安全性 形式确认：完整性、准确性、一致性、可追踪性 软件生成与变换工具 知识、能力与工程方法 分析方法学习原理知识 综合方法实现结构设计 组件综合实现模块设计 工程综合实现系统结构 能力（CPU、OS及编译系统） 依据工业标准规范 运用工程综合方法 实现工程规模系统 工业应用系统 标准规范 仪器仪表 设备环境 平台工具 软件系统 计算机学院研究与实践（2007～2013） 2006 2007 2008 2009 2010 2011 2012 组建团队 规划研究，顶层设计 精选本科生首次完成MIPS处理器开发 数字电路首轮实验 编译技术首先调整 数字电路全面调整 编译技术全面调整 自主开发统一硬件实验平台 数字电路全面实施 编译技术全面实施 全面重构硬件代码(特别是MIPS代码) OS调整，模拟器运行 OS全面实施，模拟器/硬件双平台同时实施 计组引入HDL和EDA 计组全面实施 新计组 (融合数电) 系统观点与 工程能力 计算机专业工程认证 2013 规模 形成 能力 研究目标 2006年计算机专业认证，2006年国家计算机教学示范中心，2007年获批国家教学创新实验区，2009年获批国家教学团队 研究数理逻辑、数字逻辑、计算机组成、操作系统和编译技术课程关系，通过教学和实验两个方面进行整体探讨和设计。 以MIPS指令集为基础，使得学生能够设计一台功能计算机、一套操作系统和一套编译系统。 数字逻辑 结合数理逻辑知识，讲授组合逻辑与时序逻辑原理 基于MIPS指令集，设计寄存器、加法器、移位器、控制器、多路选择器、计数器、比较器 Verilog 计算机组成 讲授计算机硬件工作原理 在部件设计基础上，实现MIPS指令集的功能型计算机系统 深化HDL语言、EDA工具应用 操作系统 讲授OS的各组成及其机理 实现MIPS的功能型OS 编译技术 讲授编译器的构造技术、实现MIPS的C编译器 计算机系统课程群体系 持续改进与实践 持续8年，2014年度国家教学成果二等奖 2006 2007 2008 2009 2010 2011 2012 2013 研制 项目 工程教育专业认证试点通过后，全院讨论人才培养 达成“系统能力培养”共识 计算机系统核心课程群建设立项 组建课程群教学团队 选拔优秀学生组建3个实验小组 学生自主开发完成MIPS处理器、小操作系统核心系统、编译器 首次调整 实施新方案(3轮次) ?加大优化比例与难度 (2轮次) 编译 技术 移植运行 环境 ?实施新方案(4轮次) 操作 系统 ? ? 重构MIPS CPU代码 实施新方案(3轮次) 融合数字逻辑(试验班) 融合数字逻辑并调整为8个实验 (1轮次) 计算机组成 实施新方案 (其余各班) 引入HDL 实施新方案(4轮次) 数字 逻辑 ? 自主开发集成环境 持续改进集成环境? ? 实验 环境 3年方案研制 5年持续实践与改进 启动 * 未来的发展，信息在其中的作用（侧重于民用）