高信頼性システムのコード分析

こんにちはHabr!この記事では、信頼性の高いシステムのコード分析について、あまり議論されていないトピックについて説明したいと思います。優れた静的分析とは何かについてHabréに関する記事はたくさんありますが、この記事では、正式なコード検証とは何かについて説明し、静的アナライザーとコーディング標準を不用意に使用することの危険性についても説明します。



信頼性を高めたソフトウェアの作成方法、方法論、開発組織へのアプローチ、ツールについて多くの論争がありました。しかし、これらすべての議論の中で失われているのは、ソフトウェア開発はプロセスであり、非常によく研究され、形式化されているということです。そして、このプロセスを見ると、このプロセスは、コードの記述/生成方法だけでなく、このコードの検証方法にも焦点を当てていることがわかります。最も重要なことは、開発には「信頼できる」ツールの使用が必要です。



この短いツアーは終了しました。コードの信頼性がどのように証明されているかを見てみましょう。まず、信頼性の要件を満たすコードの特性を理解する必要があります。「コードの信頼性」という用語は、かなり曖昧で矛盾しているように見えます。したがって、私は何も発明したくないので、コードの信頼性を評価するときは、GOST R ISO26262やKT-178Cなどの業界標準に基づいています。言い回しは異なりますが、考え方は同じです。信頼できるコードは単一の標準(いわゆるコーディング標準に従って開発され、その中の実行時エラーの数は最小限に抑えられます。ただし、ここではすべてがそれほど単純ではありません。たとえば、コーディング標準への準拠が不可能であり、そのような逸脱を文書化する必要がある場合に、標準は状況を規定します。



危険な泥沼MISRA等



コーディング標準は、潜在的に危険な可能性のあるプログラミング言語構造の使用を制限することを目的としています。理論的には、これによりコードの品質が向上するはずですよね?はい、これによりコードの品質が保証されますが、コーディングルールへの100%の準拠はそれ自体が目的ではないことを常に覚えておくことが重要です。コードが一部のMISRAのルールに100%準拠している場合、これはそれが適切で正しいことを意味するものではありません。リファクタリングやコーディング標準の違反のクリーンアップに多くの時間を費やすことができますが、コードが正しく機能しなくなったり、ランタイムエラーが含まれていると、これらすべてが無駄になります。さらに、MISRAまたはCERTのルールは通常、企業で採用されているコーディング標準の一部にすぎません。



静的分析は万能薬ではありません



規格は、コードの欠陥を見つけ、コーディング規格のコードを分析するために、体系的なコードレビューを規定しています。



この目的で一般的に使用される静的分析ツールは、欠陥の検出には優れていますが、ソースコードにランタイムエラーがないことを証明するものではありません。また、静的アナライザーによって検出されたエラーの多くは、実際にはツールの誤検知です。その結果、これらのツールを使用しても、チェックの結果をチェックする必要があるため、コードのチェックにかかる時間を大幅に短縮することはできません。さらに悪いことに、ランタイムエラーを検出できない場合があります。これは、高い信頼性を必要とするアプリケーションには受け入れられません。



正式なコード検証



そのため、静的アナライザーは常にランタイムエラーをキャッチできるとは限りません。それらをどのように検出して排除できますか?この場合、ソースコードの正式な検証が必要です。



まず第一に、あなたはそれがどんな種類の動物であるかを理解する必要がありますか?正式な検証は、正式な方法を使用したエラーのないコードの証明です。怖いように聞こえますが、実際には、マタンの定理の証明のようなものです。ここには魔法はありません。この方法は、抽象的な解釈を使用するため、従来の静的分析とは異なります。ヒューリスティックではなく。これにより、次のことがわかります。コードに特定のランタイムエラーがないことを証明できます。これらの間違いは何ですか?これらはすべて、あらゆる種類の配列オーバーラン、ゼロによる除算、整数オーバーフローなどです。それらの意味は、コンパイラがそのようなエラーを含むコードを収集するという事実にあります(そのようなコードは構文的に正しいため)が、このコードを実行すると、それらが表示されます。



例を見てみましょう。以下のスポイラーには、単純な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);







認定および認定された静的アナライザー であるPolyspaceBug 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 CodeProverの正式な検証ツールを使用して同じコードを検証しましょう。





結果の緑色は、ランタイムエラーがないことが証明されたコードです。赤-証明されたエラー。オレンジ-ツールのデータが不足しています。緑でマークされた結果は最も興味深いものです。コードの一部でランタイムエラーがないことが証明されている場合、コードのこの部分でテストの量を大幅に減らすことができます(たとえば、堅牢性のテストを実行できなくなります)。次に、潜在的なエラーと証明されたエラーの要約表を見てみましょう。



結果を見る






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やGOSTR ISO 26262などの業界標準を扱う場合、「ツールへの信頼」や「ツールの認定」などに常に遭遇します。それは何ですか?これは、プロジェクトで使用された開発ツールまたはテストツールの結果が信頼できることを示し、それらのエラーが文書化されるプロセスです。すべてが明らかであるとは限らないため、このプロセスは別の記事のトピックです。ここで重要なのはこれです。業界で使用されているツールには、このプロセスに役立つ一連のドキュメントとテストが常に付属しています。



結果



簡単な例で、古典的な静的分析と正式な検証の違いを調べました。業界標準への準拠が必要なプロジェクト以外に適用できますか?はい、もちろんできます。ここで試用版をリクエストすることもできます



ちなみに、興味のある方は、機器認証について別の記事を作ることができます。そのような記事が必要な場合はコメントに書き込んでください。



All Articles