|
果软件中的错误发现得晚，修正错误的代价就要高得多。如果有软件的静态分析工具，就可以在测试阶段之前，早期检测出错误。静态检测的结果适用于软件的各种执行方式。法国原子能委员会的系统和技术集成实验室正是采用这种方式，开发出了具有创新意义的Ｃａｖｅａｔ工具，以加强对工业应用关键软件安全性的控制。
Ｃａｖｅａｔ工具基于软件的验证技术和静态分析技术。主要探测由不具有预期特性的结果而导致的错误。也可以标志出软件执行中出错的可能性，比如无限循环和被零除。其工作原理是将需要审查的包括有数万行命令的软件与只有几行的数学公式表达结果的预期特性进行比较。根据比较，Ｃａｖｅａｔ工具提出一个数学条件。比如，为使结果为预期结果，参数ａ必须低于０。这时，使用者再检查这一参数在各种使用条件下是否都低于０。如果结果在各种条件下都低于０，便等于提出验证，证明结果与预期的特性相符合。如验证不对，工具可以指出验证失败的原因是什么。系统这时提出的假设通常证据并不完备，还需要进一步明确。
一般的静态分析软件只能检测出因除以零而导致的错误，Ｃａｖｅａｔ工具则能够明确指出发生这种错误的各种不同情况。因此，这种工具软件能够更加细致地分析出潜在错误的原因，同时还可以根据软件的使用条件，判断错误是否会产生。分析结果之所以更为明确，是因为使用者可以交互参与，而其它的工具软件完全是自动生成的。
据悉，法国空中客车公司和法国电力公司，已经在软件的开发过程中试用了这一工具，从而保证了它在工业生产中的适用性。
< 1 > < 2 >
|
