关于如何创建具有更高可靠性的软件,方法论,开发组织方法和工具,存在很多争议。但是在所有这些讨论中,所丢失的是软件开发是一个过程,并且已经进行了充分的研究和形式化。并且,如果您看一下此过程,您会发现该过程不仅关注代码的编写/生成方式,而且关注于如何验证代码。最重要的是,开发需要使用您可以“信任”的工具。
这次简短的浏览已经结束,让我们看看如何证明代码是可靠的。首先,您需要了解满足可靠性要求的代码特征。术语“代码可靠性”看起来相当模糊和矛盾。因此,我不想发明任何东西,并且在评估代码的可靠性时,我会受到行业标准(例如GOST R ISO 26262或KT-178S)的指导。措辞不同,但是思想是相同的:可靠的代码是根据单一标准(所谓的编码标准)开发的,并且其中的运行时错误数量已降至最低。但是,这里的一切并不是那么简单-标准提供了以下情况:例如,无法遵守编码标准,并且需要记录这种偏差
危险的泥潭MISRA等
编码标准旨在限制可能具有潜在危险的编程语言构造的使用。从理论上讲,这应该提高代码的质量,对吗?是的,这可以确保代码的质量,但是记住100%遵守编码规则本身并不是目的,这一点始终很重要。如果某个代码100%符合某些MISRA的规则,那么这并不意味着它是正确和正确的。您可能需要花费大量时间进行重构,清理违反编码标准的行为,但是如果代码最终无法正常工作或包含运行时错误,所有这些都将被浪费掉。此外,MISRA或CERT的规则通常只是企业采用的编码标准的一部分。
静态分析不是万能药
这些标准规定了系统的代码审查,以便发现代码中的缺陷并分析代码以用于编码标准。
通常用于此目的的静态分析工具可以很好地发现缺陷,但是它们不能证明源代码没有运行时错误。静态分析仪检测到的许多错误实际上是工具的误报。结果,由于需要检查检查结果,因此使用这些工具不会大大减少检查代码所花费的时间。更糟糕的是,它们可能无法检测到运行时错误,这对于要求高可靠性的应用程序是不可接受的。
正式代码验证
因此,静态分析器并不总是能够捕获运行时错误。如何检测和消除它们?在这种情况下,需要对源代码进行正式验证。
首先,您需要了解它是哪种动物?形式验证是使用形式化方法对无错误代码的证明。听起来很吓人,但实际上-就像是Matan定理的证明。这里没有魔术。此方法与传统的静态分析不同,因为它使用抽象解释而不是试探法。这给了我们以下内容:我们可以证明代码中没有特定的运行时错误。这些错误是什么?这些都是各种数组溢出,被零除,整数溢出等。它们的意思在于,编译器将收集包含此类错误的代码(因为此类代码在语法上是正确的),但是在运行此代码时,它们将出现。
让我们来看一个例子。扰流器下面是一个简单的PI控制器的代码:
查看代码
pictrl.c
#include "pi_control.h"
/* Global variable definitions */
float inp_volt[2];
float integral_state;
float duty_cycle;
float direction;
float normalized_error;
/* Static functions */
static void pi_alg(float Kp, float Ki);
static void process_inputs(void);
/* control_task implements a PI controller algorithm that ../
*
* - reads inputs from hardware on actual and desired position
* - determines error between actual and desired position
* - obtains controller gains
* - calculates direction and duty cycle of PWM output using PI control algorithm
* - sets PWM output to hardware
*
*/
void control_task(void)
{
float Ki;
float Kp;
/* Read inputs from hardware */
read_inputs();
/* Convert ADC values to their respective voltages provided read failure did not occur, otherwise do not update input values */
if (!read_failure) {
inp_volt[0] = 0.0048828125F * (float) inp_val[0];
inp_volt[1] = 0.0048828125F * (float) inp_val[1];
}
/* Determine error */
process_inputs();
/* Determine integral and proprortional controller gains */
get_control_gains(&Kp,&Ki);
/* PI control algorithm */
pi_alg(Kp, Ki);
/* Set output pins on hardware */
set_outputs();
}
/* process_inputs computes the error between the actual and desired position by
* normalizing the input values using lookup tables and then taking the difference */
static void process_inputs(void)
{
/* local variables */
float rtb_AngleNormalization;
float rtb_PositionNormalization;
/* Normalize voltage values */
look_up_even( &(rtb_AngleNormalization), inp_volt[1], angle_norm_map, angle_norm_vals);
look_up_even( &(rtb_PositionNormalization), inp_volt[0], pos_norm_map, pos_norm_vals);
/* Compute error */
normalized_error = rtb_PositionNormalization - rtb_AngleNormalization;
}
/* look_up_even provides a lookup table algorithm that works for evenly spaced values.
*
* Inputs to the function are...
* pY - pointer to the output value
* u - input value
* map - structure containing the static lookup table data...
* valueLo - minimum independent axis value
* uSpacing - increment size of evenly spaced independent axis
* iHi - number of increments available in pYData
* pYData - pointer to array of values that make up dependent axis of lookup table
*
*/
void look_up_even( float *pY, float u, map_data map, float *pYData)
{
/* If input is below range of lookup table, output is minimum value of lookup table (pYData) */
if (u <= map.valueLo )
{
pY[1] = pYData[1];
}
else
{
/* Determine index of output into pYData based on input and uSpacing */
float uAdjusted = u - map.valueLo;
unsigned int iLeft = uAdjusted / map.uSpacing;
/* If input is above range of lookup table, output is maximum value of lookup table (pYData) */
if (iLeft >= map.iHi )
{
(*pY) = pYData[map.iHi];
}
/* If input is in range of lookup table, output will interpolate between lookup values */
else
{
{
float lambda; // fractional part of difference between input and nearest lower table value
{
float num = uAdjusted - ( iLeft * map.uSpacing );
lambda = num / map.uSpacing;
}
{
float yLeftCast; // table value that is just lower than input
float yRghtCast; // table value that is just higher than input
yLeftCast = pYData[iLeft];
yRghtCast = pYData[((iLeft)+1)];
if (lambda != 0) {
yLeftCast += lambda * ( yRghtCast - yLeftCast );
}
(*pY) = yLeftCast;
}
}
}
}
}
static void pi_alg(float Kp, float Ki)
{
{
float control_output;
float abs_control_output;
/* y = integral_state + Kp*error */
control_output = Kp * normalized_error + integral_state;
/* Determine direction of torque based on sign of control_output */
if (control_output >= 0.0F) {
direction = TRUE;
} else {
direction = FALSE;
}
/* Absolute value of control_output */
if (control_output < 0.0F) {
abs_control_output = -control_output;
} else if (control_output > 0.0F) {
abs_control_output = control_output;
}
/* Saturate duty cycle to be less than 1 */
if (abs_control_output > 1.0F) {
duty_cycle = 1.0F;
} else {
duty_cycle = abs_control_output;
}
/* integral_state = integral_state + Ki*Ts*error */
integral_state = Ki * normalized_error * 1.0e-002F + integral_state;
}
}
pi_control.h
/* Lookup table structure */
typedef struct {
float valueLo;
unsigned int iHi;
float uSpacing;
} map_data;
/* Macro definitions */
#define TRUE 1
#define FALSE 0
/* Global variable declarations */
extern unsigned short inp_val[];
extern map_data angle_norm_map;
extern float angle_norm_vals[11];
extern map_data pos_norm_map;
extern float pos_norm_vals[11];
extern float inp_volt[2];
extern float integral_state;
extern float duty_cycle;
extern float direction;
extern float normalized_error;
extern unsigned char read_failure;
/* Function declarations */
void control_task(void);
void look_up_even( float *pY, float u, map_data map, float *pYData);
extern void read_inputs(void);
extern void set_outputs(void);
extern void get_control_gains(float* c_prop, float* c_int);
让我们使用经认证的合格静态分析器Polyspace Bug Finder运行测试,并获得以下结果:
为方便起见,我们将结果制成表格:
查看结果
|
|
|
Non-initialized variable
|
Local variable 'abs_control_output' may be read before being initialized.
|
159
|
Float division by zero
|
Divisor is 0.0.
|
99
|
Array access out of bounds
|
Attempt to access element out of the array bounds.
Valid index range starts at 0. |
38
|
Array access out of bounds
|
Attempt to access element out of the array bounds.
Valid index range starts at 0. |
39
|
Pointer access out of bounds
|
Attempt to dereference pointer outside of the pointed object at offset 1.
|
93
|
现在,我们使用Polyspace Code Prover正式验证工具来验证相同的代码:
结果中的绿色是已证明没有运行时错误的代码。红色-已证明错误。橙色-该工具没有数据。用绿色标记的结果是最有趣的。如果对于一部分代码已经证明没有运行时错误,那么对于这部分代码,可以大大减少测试量(例如,无法再进行健壮性测试)。现在,让我们看一下潜在和已证明错误的摘要表:
查看结果
|
|
|
Out of bounds array index
|
38
|
Warning: array index may be outside bounds: [array size undefined]
|
Out of bounds array index
|
39
|
Warning: array index may be outside bounds: [array size undefined]
|
Overflow
|
70
|
Warning: operation [-] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Illegally dereferenced pointer
|
93
|
Error: pointer is outside its bounds
|
Overflow
|
98
|
Warning: operation [-] on float may overflow (result strictly greater than MAX FLOAT32)
|
Division by zero
|
99
|
Warning: float division by zero may occur
|
Overflow
|
99
|
Warning: operation [conversion from float32 to unsigned int32] on scalar may overflow (on MIN or MAX bounds of UINT32)
|
Overflow
|
99
|
Warning: operation [/] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Illegally dereferenced pointer
|
104
|
Warning: pointer may be outside its bounds
|
Overflow
|
114
|
Warning: operation [-] on float may overflow (result strictly greater than MAX FLOAT32)
|
Overflow
|
114
|
Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
115
|
Warning: operation [/] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Illegally dereferenced pointer
|
121
|
Warning: pointer may be outside its bounds
|
Illegally dereferenced pointer
|
122
|
Warning: pointer may be outside its bounds
|
Overflow
|
124
|
Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
124
|
Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
124
|
Warning: operation [-] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
142
|
Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
142
|
Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Non-uninitialized local variable
|
159
|
Warning: local variable may be non-initialized (type: float 32)
|
Overflow
|
166
|
Warning: operation [*] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
Overflow
|
166
|
Warning: operation [+] on float may overflow (on MIN or MAX bounds of FLOAT32)
|
该表告诉我以下内容:
肯定会发生第93行上的运行时错误。其余警告则告诉我,我是否正确配置了验证,或者我需要编写安全代码或以其他方式克服它们。
看起来,形式验证非常酷,应该对整个项目进行不可控制的验证。但是,与任何工具一样,存在一些限制,主要与时间成本有关。简而言之,正式验证很慢。太慢了。性能受到抽象解释本身和要验证的代码量的数学复杂性的限制。因此,您不应尝试快速验证Linux内核。Polyspace中的所有验证项目都可以分为可以相互独立验证的模块,并且每个模块都有自己的配置。也就是说,我们可以分别调整每个模块的验证完整性。
工具中的“信任”
当您处理诸如KT-178C或GOST R ISO 26262之类的行业标准时,就会不断遇到诸如“信任工具”或“工具资格”之类的问题。它是什么?在此过程中,您可以证明该项目中使用的开发或测试工具的结果可以信任,并且可以记录其错误。此过程是另一篇文章的主题,因为并非所有内容都是显而易见的。这里的主要内容是:行业中使用的工具总是附带一系列有助于此过程的文档和测试。
结果
通过一个简单的示例,我们研究了经典静态分析和形式验证之间的区别。可以将其应用到需要遵守行业标准的项目之外吗?是的,当然可以。您甚至可以在这里索取试用版。
顺便说一句,如果您有兴趣,可以撰写有关仪器认证的单独文章。如果需要这样的文章,请在评论中写。