课程简介 Course Introduction

形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整,有助于增加软件开发人员对系统的理解,因此形式化方法是提高软件系统,特别是Safety-Critical系统的安全性与可靠性的重要手段。最早的形式化方法是逻辑与逻辑推理,它的目标是使推理机械化。从广义上讲,这一目标受到许多挫折,比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)。但是在一些实际应用上,逻辑方法和自动推理还是起着非常大的作用。

教学大纲 Teaching Syllabus

从广义上讲,形式化方法是借助数学的方法来解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言,形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定,或证明该表达式具有某种性质。


留言板 Message Board
条留言  共

  • 参与互动
    Interaction

  • 扫码加入课程
    Scan QR Code
需要验证您的身份,请输入请求信息:
  • 学号号:
  • 班级选择:
  • 附注信息:

扫一扫二维码,快速加入本课程!

放大二维码 查看使用方法
课程
引导