静态分析验证工具

续上

考虑到字面上的近似，几个名词提前说明，当然，这仍然是我个人的看法：

时序逻辑temporal logic：是一种逻辑属性，而不是一种时间属性，是有关真假的定性描述，而不是有关长度的定量描述。

时间性timeliness：有关时间的属性，不仅是先后顺序，而且有间隔长度，甚至是绝对时间坐标要求。

通常讲时序，如讲功能和时序，尤其是在电子电路中，含义是“时间轴上的序列”，是广义的，因此是timeliness、timely，包括时间上的顺序及定时。而在软件领域，讲时序含义是“时间上的顺序关系”，其实是一种先后关系，更准确的用语是sequential、order、sequence。

无论如何，用语是很区分的。一般讲时序是定性的，即“顺序”；而讲实时，则必然是“时间序列”，是定量的，包括先后关系sequential relation+间隔长度interval；讲通信时，时序的含义是“时间上的协调”，可能只是先后关系上的协调，也可能是指定间隔长度的协调。

有关可检验范围的说明：

安全性safety：这是被广泛支持的一种属性，包括大多数用户断言、死锁及诸多LTL属性，可以通过检查一个有限的序列来验证，通常以“always”的形式表达，但是序列中使用的状态必须是past 时态的，也就是说不能对“将来”要求“安全性”。

活性liveness：这个无法通过检查一个有限序列来验证，因为这个有限的前缀后面总是可以跟一个无限的序列，也就是说，在可达性图中找可接受状态。

FeaVer/Modex/SPIN工具链

这算是软件验证工具的一个强强组合了，以Modex作为总称，由贝尔实验室的model checking大牛G. J. Holzmann打造。其中，FeaVer做为前端，提供从ANSI-C编写的代码中提取异步并发模型的HMI；而Modex是完成该任务实际的Model Extractor，生成Promela版的并发模型描述语言；SPIN作为后端，能够对Promela语言描述的并发模型进行多种线性时序逻辑（LTL）属性检验，找出存在的缺陷。整个工具链可以实现对ANSI-C程序进行逻辑性检验，包括对用户自定义的LTL属性的检查。

这里需要指出的是，modex虽然打通了软件验证过程的主动脉，但是仅限于LTL属性，对于以时间约束为重要需求项目的嵌入式控制领域软件的实时属性是不适用的。

就使用Modex而言，不需要了解什么工作原理，但是需要了解它的内部工作流和外部接口。为了能够trap用户断言的违例，FeaVer先对C源代码进行插桩，例如数组越界、指针引用无效这类缺陷的断言；另一方面，由于SPIN的并发是完全无控制的，因此FeaVer插桩可以强化、操控这种并发交替的模式。在提取SPIN中的Process概念时，又涉及到代码块映射到Process的粒度，这也是在FeaVer插桩时决定的，通过决定哪些代码块要插桩、哪些不插，可以控制检验的深度和建模的粒度，二者需要平衡。【Modex FAQ】

当然，用于量化时间属性检验的验证工具也是有的，在SPIN基础上就有RT-SPIN。但是，think it critically，为了量化系统的时间属性，并不一定要采用这种直接修改checker底层算法的做法，这相当于直接在验证算法中引入了时间因子。正如微软的Leslie Lamport大牛指出的，Real-time Model Checking is Really Simple!就是直接用untimed的并发系统描述语言来表达时钟的概念，所谓“显式”时间化的方法。其实，我也是这么想过，也试过，但是在这条思路上完全又造出一种新的描述语言TLA+及其工具TLC，那就只有大牛了。

这个想法相当容易想到，我最初就是为了描述系统中的定时器角色，平行添加了一个进程，内容就是不断计数，满了后做某个动作。但是这样存在一个问题，因为SPIN的并发调度是完全随机的，那么有可能一个进程反复触发，推动时钟，但是定时器进程却永远没有机会看一看自己的时钟，是否到时间了，象定时中断这种系统行为还是描述不了。这是一个失败的实现方式。然后，第二个方案是，给每个进程的每条原子级语句前插入了一个累加及上限检查的原子性语句段，直接模拟中断的真实硬件动作，相当于加入了一个中断周期，确保时钟的最高优先级。

我还没去查TLC是怎么做的，也就不知道，“显式的”时钟跟“隐式的”时钟有什么不同，但现在看来，在以中断为主要并行方式的嵌入式控制领域，显式的时钟已经足够简便、足够用了。

C.OPEN/ANNOTATOR/CADP工具链

也相当具有吸引力，它的基础是强大CADP分布式进程库。C.OPEN是一个C程序的模型提取器，建立在CADP基础上，输出为LTS；ANNOTATOR是一个影响流静态分析器，以LTS为输入。它不仅拥有直接处理C代码的能力，而且将静态分析技术引入进来，非常具有启发性。同时，建立在CADP基础上，以便于利用各种形式化理论，非常有潜力的一个组合。

静态分析技术和模型检验技术的共性在于，都是为了在运行前找出程序中存在的某种缺陷，归属于静态测试。但是，静态分析侧重于数据的量化计算，模型检验侧重于逻辑属性的验证，一个是定量的，一个是定性的，二者之间几乎不存在交集。而看看Christophe Joubert的这篇论文的引言就知道了，最近５年就有一群天才的人将两者联系起来了，先是有人想到用静态分析得到的数据流信息降解直接由程序代码转换过来的模型状态空间，接着就有人想到反过来用模型检验的方法来做静态分析。

其它的工具还有Frame-C，说是要提供为C提供一个类似eclipse支撑环境，但却是用OCaml写的……

还有bogor，说是要提供一个模型检验工具的可扩展的框架，和上面的提法差不多……

其实，eclipse人家本身就有这样做法，例如CDT的某个教程。

Well,回过头来，唯一有点吸引力的是bogor所谓的框架，Java实现，文档详细，很有指导意义。另外就是Modex的某些模块，可能可以参考一下思路，考虑如何用bogor的框架来实现。