Formal methods

  • 形式规范(Formal specification)是更普遍的技术集合的一部分，这些技术被称为“形式化方法”
  • 这些都是基于软件的数学表示和分析
  • 形式化方法包括
    • 形式规范 Formal specification
    • 规格分析与证明 Specification analysis and proof
    • 转型发展 Transformational development
    • 程序验证 Program verification

Formal Specification

  • 形式规范的目标：

    • 完全的
    • 持续的
    • 简洁的
    • 明确的
    • 有效——准确说明用户想要什么

  • 基于形式语义模型的规范

  • 什么是语义？ semantics

    • 语义意味着“意义”

    • 形式语义：用数学表达的意义

    • 形式语义模型：数学中语言的完整语义定义

    • 什么数学？

      • 离散数学！

    • 形式语义允许各方之间进行可靠的通信 dependable communication

  • 什么是形式语义模型？ formal semantic model

Types Of Languages
  • 程序：Procedural
    • 由计算机要执行的所需动作序列定义的计算
    • 大多数高级语言都是程序化的
  • 声明：Declarative
    • 由计算机应处于的期望状态定义的计算
    • 许多规范语言都是声明性的
  • 语言的最大区别在于：
    • 声明式(Declarative)：不说如何，只说什么
    • 程序性的(Procedural)：什么都不说，只说怎么做

  • Library Example: Informal Statement 图书馆示例：非规范声明

    • 一本书可以成堆、保留或借出

    • 如果一本书在书架中或被保留，则可以请求

    • 我们想

      • 形式化概念和陈述
        • 证明一些定理以获得对规范正确的信心

    • 首先让我们形式化一些概念 S: the book is in the stacks R: the book is on reserve L: the book is on loan Q: the book is requested

    • 如果需要一本书，那么它就在书架上或保留

Resolution Refutation 归结法
  • 一旦定理证明者表明否定目标(negated goal)与给定的公理集不一致，那么原始目标必须是一致的。
  • 这证明了定理

例子

  • 解析原则(resolution principle)，描述了一种在最小替换的条款数据库中查找矛盾的方法
  • 归结法通过否定要证明的陈述并将否定的目标添加到已知或已假定为真的公理集合来证明定理
  • 然后它使用推理的分解规则来证明这导致了一个矛盾

步骤

  • 把前提或公理变成从句形式
  • 将要以从句形式证明的内容的否定添加到公理集合中
  • 一起解析这些子句，产生从它们逻辑上遵循的新子句
  • 通过生成空子句产生矛盾
  • 用于产生空子句的替换是那些否定目标的反面为真的替换

演绎可以用一棵树来表示——演绎树。

  • 例子1

    • We wish to prove that “Fido will die” from the statements that

    • “Fido is a dog” and “all dogs are animals” and “all animals will die”

    • Convert these predicates to clause form

    • Negate the conclusion that fido will die ¬die(fido)

  • 例子2

    • Jack owns a dog.
    • Every dog owner is an animal lover.
    • No animal lover kills an animal.
    • Either Jack or Curiosity killed the cat, who is named Tuna.
    • Did Curiosity kill the cat?

  • 例子3

Introduction

形式方法 Formal methods

  • 提高软件质量，减少错误
  • 只有少数软件是用形式化方法开发的
    • 成功的软件工程
    • 市场变化
    • 形式方法的范围有限
    • 形式方法的可扩展性有限
  • 应用于某些领域，如关键系统

形式规范 Formal specification

  • 紧接着系统要求
  • 详细需求规范和形式规范之间的紧密反馈循环

Software development costs with formal specification

形式规范语言 Formal specification languages
  • 代数方法 Algebraic approach
    • 系统是根据操作及其关系来描述的
    • Larch(Guttag et al., 1985,1993), OBJ(Futatsugi et al., 1985), Lotos(Bolognesi and Brinksma, 1987)
  • 基于模型的方法 Model-based approach
    • 系统模型是使用数学结构（例如集合和序列）构建的，系统操作由它们如何修改系统状态来定义
    • Z(Spivey, 1992), VDM(Jones, 1980), B(Wordsworth, 1986), CSP(Hoare, 1985), Petri Nets(Peterson, 1981)

接口规范 Interface specification

  • 大型系统被分解为子系统，这些子系统之间具有明确定义的接口

  • 子系统接口的规范允许不同子系统的独立开发

  • 接口可以定义为抽象数据类型或对象类

  • 形式化规范的代数方法特别适用于接口规范

Sub-system interfaces

Sub-system interface specification
  • 代数方法
    • 接口类似于对象类
      • 介绍，声明指定的排序（类型名称）
      • 描述，其中操作被非正式地描述
      • 签名，定义对象类或抽象数据类型的接口语法
      • 公理，通过定义一组表征抽象数据类型行为的公理来定义操作的语义

Recursion in specifications

操作通常以递归方式指定。

例子：一个扇区

  • 表示受控扇区的对象上的关键操作是
    • Enter。 在管制空域增加一架飞机；
    • Leave。 将飞机移出管制空域；
    • Move。 将飞机从一个高度移动到另一个高度；
    • Lookup。 给定飞机标识符，返回其当前高度；
Primitive operations
  • 有时需要引入额外的操作来简化规范
  • 然后可以使用这些更原始的操作定义其他操作
  • Primitive operations
    • Create。 使扇区实例存在
    • Put。 添加一架没有安全检查的飞机

Behavioral specification

  • 基于模型的规范 Model-based specification
  • 抽象状态机语言 (AsmL) Abstract State Machine Language

Abstract State Machine Language (AsmL)

  • AsmL 是一种可执行的规范语言，用于对数字系统的结构和行为进行建模
  • 抽象帮助我们将复杂的问题简化为可管理的单元，并防止我们迷失在细节的海洋中
  • AsmL 提供了多种功能，允许您以非常经济、高级的方式描述系统的相关状态
State transitions

机器的行为（它的运行）总是可以被描述为由状态转换链接的状态序列

Evolution of state variables 状态变量的演化

state variables: (Name, Value)

例子：

图表显示了机器的运行，该机器对订单的处理方式进行建模

  • 每个过渡操作：
    • 可以看作是在当前状态上调用机器的控制逻辑的结果
    • 计算子序列状态作为输出
Control Logic

机器控制逻辑是一个黑匣子，它以状态字典 S1 作为输入，并给出一个新字典 S2 作为输出

两个字典 S1 和 S2 具有相同的一组键，但与每个变量名称关联的值在 S1 和 S2 之间可能不同

  • 例子：读取文件

  • 例子：图像表示

​

Behavioral specification
  • Z Schema
    • Schema signature
    • Schema predicate