本文主要尝试运行一个kind2的例子，来展示kind2的验证效果。

Kind2

Kind2是一个多引擎、并行、基于SMT的自动模型检查工具，用于Lustre程序的安全性验证。

Kind2是一个命令行工具，接受一个Lustre文件作为输入，输出所有输入中的属性是否为真。为了便于外部工具处理，结果可以以JSON和XML格式输出。

参考网站：Kind 2 (uiowa.edu)

Kind2在线工具：Kind (uiowa.edu)

具体安装教程见：Linux系统kind2安装教程 | Fifish’s BBlog (hififish.github.io)

  1. 创建.lus文件

    在文件夹中建立一个.lus文件，并进行编辑。

    1
    $ vi example1.lus

    用例选自：Lustre Input (uiowa.edu)

    下面的示例声明了两个节点greycounter和intcounter，以及调用这些节点并验证其输出是否相同的观察者节点top。节点顶部用–%MAIN；使它成为顶部节点（这里是多余的，因为它是最后一个节点）。“–%PROPERTY OK；”表示我们要验证布尔流OK始终为真。

    image-20210816210041645

  2. 在docker上运行Kind2

    要在系统上的文件上运行Kind2，建议将此文件所在的文件夹作为volume装入。

    volume使用指南：Use volumes | Docker Documentation

    运行：

    1
    docker run -v <absolute_path_to_folder>:/lus kind2/kind2:dev <options> /lus/<your_file>
    • <absolute_path_to_folder> 是指.lus文件所在文件夹的路径；
    • <your_file> 是将用Kind2运行的文件；
    • <options> 是你选择的Kind2操作。//可不填，执行默认操作

    *注意：

    • 文件夹必须是绝对路径这一项是docker的约束；
    • 挂载点/lus是任意的，只要它与最后一个参数/lus/一致就无所谓。但是，为了避免名称与容器中已存在的文件夹冲突，建议使用/lus；
    • 如果您希望运行kind2的最新版本而不是开发版本，请将kind2:dev替换为kind2；
    • docker run不会将本地Kind 2映像更新为最新映像：相应的docker pull命令会更新

    运行成功：

    image-20210817140012302