《欧洲高校计算机专业的形式化方法课程教学.doc》由会员分享，可在线阅读，更多相关《欧洲高校计算机专业的形式化方法课程教学.doc（5页珍藏版）》请在三一文库上搜索。
1、欧洲高校计算机专业的形式化方法课程教学文献标识码：B 形式化方法是基于严密的、数学上的形式机制的计算机系统研究方法。从20世纪90年代开始，计算机学科相关专业的形式化方法的教育引起了欧美教育界的高度重视和关注。欧洲的英国、德国、法国、意大利、荷兰、西班牙等国家的高校相继为研究生开设了形式化方法方面的课程，并推广至本科生教育。从20世纪90年代中期开始，美国高校也开展了形式化方法教育研究，并在美国顶尖的35所大学的计算机学科实施了研究生和本科生的教育实践。 IEEE-CS和ACM联合任务组于2005年9月提交了计算教程CC2005(Computing Curricula 2005)最终报告，该报
2、告的软件工程分册CCSE(Computing Curriculum- Software Engineering 2004)将“软件工程的形式化方法(Formal Methods in Software Engineering)”列为一门核心课程。CC2005最终报告的推出对计算机学科相关专业的形式化方法教育产生了重要的影响。 欧洲形式化方法协会于2001年成立了专门的形式化方法教育研究分会FME-SoE(Formal Methods Europe Association - Subgroup on Education)，目的在于研究并提出高等院校本科生形式化方法教育的知识体系及课程内容。该组织
3、于2004年11月发布了对欧洲11个国家、58所高等院校中的117门形式化方法教育相关课程的调研报告。 1形式化方法知识体系 FME-SoE组织对欧洲高等院校本科生的形式化方法教育进行了调查分析，将形式化方法分划为6个知识领域和15个知识单元。图1给出了该分析过程中形式化方法的知识体系。 图1 形式化方法知识体系 形式化方法(FM-Formal Method)知识体系中的6个知识领域为： 基础(Foundations)； 形式化规格(Formal specification paradigms)； 正确性验证及演算(Correctness, verification and calculati
4、on)； 形式化语义(Formal semantics)； 可执行规格支持(Support for executable specification)； 其他(Other Topics)。 6个知识领域包括15个知识子领域或者知识单元：FM01形式化方法的集合理论/拓扑基础(Set-theoretic/topological foundations of Formal Methods)；FM02 形式化方法的逻辑基础(Logical foundations of Formal Methods)；FM03 形式化方法的类型理论基础(Type-theoretic foundations of Fo
5、rmal Methods)；FM04 形式化方法的代数基础(Algebraic foundations of Formal Methods)；FM05 面向性质规格(Property oriented specification)；FM06 面向模型规格(Model oriented specification)；FM07 多范式规格(Multi-paradigm specification)；FM08 构造正确性(Correct by construction)；FM09 验证正确性(Correct by verification)；FM10 机器检验正确性(Correct by machi
6、ne checking)；FM11 求精技术(Refinement techniques)；FM12 程序语言语义(Programming language semantics)；FM13 形式化分布式、并发、移动(Formalizing distribution, concurrency and mobility)；FM14 声明式程序设计(Declarative programming)；FM15 其他。这些知识单元包含的知识点如表1所示。 2 形式化方法课程 形式化方法教育过程中，相关形式化方法工具的支持是非常重要和必要的。欧洲高等院校在形式化方法研究和教育过程中，开发了许多相关工具。形
7、式化工具有：Actress、Alloy、AtelierB、B-Toolkit(Btlk)、BDDC、CADP、CADiZ、CASL、Coq、CommUnity、CWB、ESCJava、FDR、FuZZ、GHC、Gofer、Hugs、HOL、集成网络分析器(INA)、Isabelle、IVDM、Lotrec、LTSA、NuSMV、Petri网程序设计环境(Petri)、PVS、PicT、RAISEtools、RAT、RML、SPIN、T-Logic、TRIO、UPAAL、VDMT、WHY、ZANS、ZEVES、ZTC等已在相关课程教学中得到使用。在这里，我们对已开设课程总结如表2所示。对这些课程
8、进行频次统计分类分析，可以发现：知识单元FM06、FM02和FM13具有较高开课率，分别为52门、27门和27门；语言Z和B在教学中得到了较多介绍，分别为16门和15门；形式化方法工具SPIN和VDMT得到了较多使用，均为6门。 3 结语 形式化方法教育得到欧、美国家高等院校的重视和大力推广不过是十余年的时间，建立完善的知识体系和课程教学内容还需要进一步的努力。从欧洲58所高校的课程开设情况来看，虽然形式化方法教育得到了大范围的实施，但是课程内容、授课教材、辅助工具等还比较散杂，建立形式化方法课程的知识内容规范、编写相关规范指导下的教材、开发相关规范指导下的辅助工具，是亟待解决的问题。 形式化方法的工业应用需求和教学过程实践的经验积累，已愈来愈体现出计算机相关专业形式化方法教育的必要性和可行性。国内计算相关专业的形式化方法教育还相当薄弱，尚未在高等院校得到有效推广和实施。计算机相关专业形式化方法课程教学的有效推进还有赖于课程教材、实验环境、支撑工具以及应用环境等方面的突破。