形式化验证1——modex工具学习

modex，即model eXtractor，由bell实验室开发，基于spin的模型检测工具，modex通过自定义的test harness来从C源代码中抽取出需要验证的spin模型。然后调用spin进行处理，最后编译spin处理过的C代码，生成名为pan.exe或者pan的应用程序。

1.安装

下载地址：http://cm.bell-labs.com/cm/cs/what/modex/ http://spinroot.com/modex/

从该网站上下载源代码包，然后按照教程一步一步进行下去即可。主要需要flex和bison这两个工具。

由于modex需要调用spin的功能，因此，需要去http://spinroot.com/spin/Man/README.html下载spin。

modex和spin在ubuntu和windows下的cygwin环境下，皆可使用。但是，在cygwin情况下，需要调用dos2unix_modex_.run转换一下该文件的格式。

modex验证工具的调研报告

1.简介

modex，又名modexextractor。顾名思义，它能够根据用户需求从ANSI—C语言的代码中抽取出需要验证的目标模型。它是用标准C实现的，其检测目标是标准的C语言，不能处理其他语言。modex以spin为基础，它从源代码中抽取出使用promela定义的模型，即自动机模型，然后在该模型上，根据定义的属性（属性也被转化为自动机）使用spin进行程序属性的验证。

2.验证对象

Ø modex是ANSI-C程序模型抽取工具

Ø modex主要用于多线程和并发程序的验证

Ø modex可以链接多种文件格式

Ø 源代码.c文件

Ø 目标文件.o文件

Ø 共享目标文件.so或者.a文件

3.主要方法与思想

modex需要用户自定义模型抽取文件，默认的后缀名是.prx。在prx文件中，可以使用一系列命令定义如何从源代码中抽取模型，以及在后续的编译过程中需要链接的目标文件。

Prx文件中经常使用的命令如下：

图1:prx文件常用命令

用户按需从源代码中抽取出模型后，使用底层的模型验证工具spin来进行验证。抽取出的模型文件默认为文件名为model。它是用promela语言定义的，可以支持多线程并发执行的程序，这也正是modex工具的主要方向。在生成需要的模型后，使用spin对抽取出的模型进行转化，最后生成命名为pan的程序。pan是由spin工具生成的文件进行编译得到的，用户无需手动修改该程序。最后，执行pan程序，该程序会显示当前模型的错误。通过加上-r或者-C选项可以显示详细出错的代码位置和信息。

modex会做三种基本的检查：

ü 空指针引用

ü 数组越界

ü 未初始化变量

在上述三种基本检查的基础上，modex可以检测另外的三种assert属性，分别是：

ü assert(expression)：判断expression能否为真

ü assert_r(expression)：检查expression能否在该assert_r语句执行后的有限执行过程中变为真

ü assert_p(expression_p,expression_q)：类似于LTL中的pWq公式

以上一系列编译步骤可以由modex提供的命令feaver_cmd完成，该命令需要prx文件作为参数，完成模型抽取和验证的工作。也可以使用modex提供的GUI执行这些步骤。通过使用GUI，用户可以精化需要抽取的模型，更加方便和友好的进行模型验证。

4.附加属性

modex除了以上的检查和属性之外，通过使用timeline属性和LTL来增强该工具的检查能力。

ü timeline属性是指与时间相关的事件的发生关系，以及定义在关系上的约束组成的属性。它是LTL的一个子集

ü LTL是指线性时序逻辑，modex通过spin支持LTL属性的验证

以上两种扩展属性会被转化为spin定义的never claim，即自动机的promela语言的定义。在需要验证的模型上，检测neverclaim是否满足。

5.优缺点

优点：

Ø 支持并发和多线程程序

Ø 支持动态链接库和目标文件以及从多文件中抽取模型

Ø 支持LTL属性和timeline属性，扩大了验证的范围

缺点：

Ø 学习曲线陡峭

Ø 验证效率得不到保证，即模型的复杂度受到用户定义的prx文件影响。prx文件决定模型的精化程度，进而决定了验证效率

Ø LTL和timeline属性使用很复杂

6.总结

modex可以检测并发和多线程程序，能够根据用户定义的模型抽取文件prx，从多个源文件中抽取出使用promela语言定义的模型，在根据用户定义的属性，执行属性验证。modex检查的属性有很多种类，包括基本的类型检查和一些高级的LTL以及timeline属性。最后，根据属性进行模型验证，检测模型是否满足定义的属性。从网上的资料可以看出，该工具可以应用在大规模的程序属性验证。

Modex工具的主要流程是：

Ø C源代码

Ø 定义prx文件：测试驱动文件

Ø 抽取模型：将源文件转化为spin自动机模型

Ø 定义需要验证的属性：转化为自动机

Ø 生成模型检测的目标代码：用于执行的标准C代码

Ø 执行验证：对目标代码编译和执行

Ø 反馈结果：错误路径和变量状态

其流程图如图2。

图 2：modex执行流程图

形式化验证1——modex工具学习相关推荐

FPGA形式化验证工具OneSpin360学习笔记（一）
目录 OneSpin360图形界面一致性检查举例等价性检查举例 Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具.它以强大.高性能的形式化验证引擎为基础,能够覆 ...
成都链安重磅出品 | 基于VS Code插件的智能合约自动形式化验证工具Beosin—VaaS『离线免费版』...
11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin-VaaS,该版本基于流行的开发工具VS Code插件,供广大开发者免费使用.获得方式如下,欢迎体验使用: https: ...
形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
Scyther形式化验证工具简单教程
Scyther形式化验证工具 Scyther是一种自动化的安全协议验证工具.在协议的安全性验证方面有着广泛的应用. 下面介绍其安装方法以及使用教程. 安装方法 Scyther工具在Windows 10 ...
操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(7) - C代码的自动验证（转载）
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍,基础好的同学已经可以基于前面的知识开始自己的工作了. 对于只学过离散数学,而 ...

形式化验证1——modex工具学习

形式化验证1——modex工具学习相关推荐

最新文章

热门文章