计算机各专业研究生选修课,秋季开课。

形式化方法是一种基于数学的软件和系统开发方法,研究如何把(具有清晰的数学基础的)严格性(描述形式、技术和过程等)融入软件开发的各个阶段:规范、设计、验证与演化等。该方法日益受到计算机界和工业界的高调重视。形式化方法是计算机专业一门重要的专业基础课,特别是计算机科学专业必修课,也是软件工程专业和信息管理专业一门重要的基础课。通过本课程的学习,使学生了解形式化方法的基本理论和基本原理,掌握软件形式规格,能应用基本形式化方法验证程序正确性。学会用“数学思维”去思考和用“形式化方法”去处理软件和系统开发过程的程序验证问题。

计算机学院专业学位必修课程。

Program verification is a fundamental theory in proving correctness of a program. Model checking is an important and popular technique for automatically verifying correctness properties of finite-state systems. This course mainly focuses on the fundamental principles and methods for model checking. This course includes the syntax and the semantics of linear temporal logic (LTL), the syntax and the semantics of computation tree logic (CTL), principles of reasoning-based program verification, and methods of model checking in applications etc.

密码学与网络信息安全是一门研究生专业选修课。我们的社会已经进入了信息时代,电子商务、事务处理以及电子政务活动的开展,对在开放的网络特别是Internet中,实现安全通信的需求正迅速增加。密码技术是网络信息安全中的关键技术,实践表明它的有效使用可以极大地提高计算机与网络的安全性。课程为计划从事信息安全理论研究和工程实践的研究生提供基础指导。课程通过对密码理论、密码算法、网络安全协议、网络安全标准的讲授,使学生理解并掌握运用密码学的方法解决网络与信息安全问题的基本知识并具备从事计算机安全系统设计、开发、管理的基本技能。

嵌入式计算机系统是指以应用为核心,以计算机技术为基础,其软硬件可配置,对功能、可靠性、成本、体积、功耗有严格约束的一种专用计算机系统。

通过本课程的学习,首先使学生全面了解嵌入式系统的概念、组成及特点,硬件平台构建,嵌入式操作系统、网络技术的相关知识;掌握嵌入式计算机系统的设计原则及设计步骤;深入了解嵌入式系统各个组成部分具体的设计方法,包括:嵌入式处理器的选择原则,总线设计,内存储器的设计,各种常用外设接口的设计,系统的可靠性设计,系统的调试等。学生在完成本课程的学习后,能独立设计嵌入式计算机系统。

软件设计自从计算机诞生之日起,就存在着显式或是隐式的危机。而1968年,在Garmish召开的国际软件工程会议上,人们迫切地感到了软件危机给计算机软件产业的发展带来的巨大阻力。软件危机的两个最大的问题便是:随着计算机软件技术的日新月异,软件的规模越来越大,软件复杂度越来越高。伴随着这两个问题的日益突出,整个软件系统结构的设计与规格说明便显得比在早期软件开发中占有重要地位的算法选择和计算问题的数据结构更为重要。代码级别的软件复用已经远远不能满足大型软件开发的需求。由此便引入了软件体系结构这一概念。

通过学习该课程,帮助研究生了解计算机软件体系结构概念,初步掌握软件系统构架的分析与设计方法,提高软件设计的基本素养。

计算机综合实验(MapReduce)通过目前云计算研究与应用中广泛采用的MapReduce编程模型,解决大规模数据的高效率并行分布式处理问题,使用开源的Hadoop作为MapReduce开发平台,使用Eclipse作为开发工具,以此达到锻炼工程实践能力,培养综合实验素质的目的。

In Computer Science and Information Science, Ontology is a formal representation of knowledge as a set of concepts within a domain, and the relationships between those concepts. Ontology is the basics of knowledge representation and automated reasoning in computer systems. The theory of ontology can be applied as the method of knowledge representation and automated reasoning in the fields of Artificial Intelligence, System Engineering, Software Engineering, Bioinformatics, and Library Science. This course, taking the Semantic Web as an example, introduce and discuss the state-of-the-art theories, methods, and frontier technologies about the information representation and data management, knowledge representation and ontology languages and their querying and reasoning on the current Web.

教授经典数据逻辑、模态逻辑、构造性逻辑等语义、语法、推理理论、独立性、完备性、可靠性等知识。

一、课程内容简介

人工智能是多学科的交叉,涉及到计算机科学、计算机工程、数学、哲学、心理学、神经生理学、进化论、控制论、系统论、信息论、语言学等诸多领域,其目标是研究如何人工制造智能机器或智能系统,用来模拟智力活动、延伸人的智力。

通过本课程的学习,使研究生掌握人工智能的学科范畴、发展历史与发展趋势、智能问题的描述与求解方法、状态空间搜索的控制策略、博弈算法、命题逻辑与谓词逻辑、产生式系统、语义网、框架等知识表示方法、归结推理方法与演绎推理方法、 PROLOG 语言、不确定推理方法、专家系统、机器学习即知识获取方法、神经网络、自然语言处理等,并对人工智能的新思路、新理论、新方法有所了解。

本 课程的特点是涉及的知识范畴广,多学科知识的交叉性强,既有宽泛的概念介绍,也有严格缜密的逻辑演算;既进行思维开放的科学研究与探讨,也给出解决具体工程问题的实用方法。 本课程的学习对于拓展研究生的知识面,培养逻辑思维能力和创新能力有一定的积极作用。

In the course, a new software development method, user-centered design, is introduced. The essence of user-centered design is analyzed and the principle, methodology and real cases of user-centered design are included the course.

By learning the course, students can comprehend the basic theory of parallel computer model, principles of scalable etc., grasp the architecture, organization technology, interconnect and communication techniques of parallel computer, establish solid fundamentals in parallel computer.

Textbook : Computer Architecture: A Quantitative Approach by Patterson & Hennessy