Analisis kode sistem keandalan tinggi

Halo Habr! Pada artikel ini, saya ingin berbicara tentang topik yang agak sedikit dibahas tentang analisis kode untuk sistem keandalan tinggi. Ada banyak artikel di Habré tentang apa itu analisis statis yang baik, tetapi dalam artikel ini saya ingin berbicara tentang apa itu verifikasi kode formal, dan juga menjelaskan bahaya penggunaan penganalisis statis dan standar pengkodean yang sembrono.



Ada banyak kontroversi tentang bagaimana membuat perangkat lunak dengan peningkatan keandalan, metodologi, pendekatan organisasi pengembangan, alat dibahas. Namun di antara semua diskusi ini, yang hilang adalah bahwa pengembangan perangkat lunak adalah sebuah proses , dan dipelajari serta diformalkan dengan cukup baik. Dan jika Anda melihat proses ini, Anda akan melihat bahwa proses ini tidak hanya berfokus pada bagaimana kode ditulis / dibuat, tetapi juga pada bagaimana kode ini diverifikasi. Yang terpenting, pengembangan membutuhkan penggunaan alat yang dapat Anda "percayai".



Tur singkat ini telah berakhir, dan mari kita lihat bagaimana kode tersebut terbukti dapat diandalkan. Pertama, Anda perlu memahami karakteristik kode yang memenuhi persyaratan keandalan. Istilah "keandalan kode" terlihat agak kabur dan kontradiktif. Oleh karena itu, saya memilih untuk tidak menemukan apa pun, dan ketika menilai keandalan kode, saya dipandu oleh standar industri, misalnya, GOST R ISO 26262 atau KT-178C. Kata-kata di dalamnya berbeda, tetapi idenya sama: kode yang andal dikembangkan sesuai dengan standar tunggal (yang disebut standar pengkodean ) dan jumlah kesalahan runtime di dalamnya diminimalkan. Namun, semuanya tidak sesederhana itu di sini - standar mengatur situasi ketika, misalnya, kepatuhan dengan standar pengkodean tidak dimungkinkan dan penyimpangan seperti itu perlu didokumentasikan



MISRA rawa berbahaya dan sejenisnya



Standar pengkodean dimaksudkan untuk membatasi penggunaan konstruksi bahasa pemrograman yang berpotensi berbahaya. Secara teori, ini seharusnya meningkatkan kualitas kode, bukan? Ya, ini memastikan kualitas kode, tetapi selalu penting untuk diingat bahwa kepatuhan 100% dengan aturan pengkodean bukanlah tujuan itu sendiri. Jika kode tersebut 100% konsisten dengan aturan beberapa MISRA, maka ini sama sekali tidak berarti kode tersebut baik dan benar. Anda dapat menghabiskan banyak waktu untuk melakukan refactoring, membersihkan pelanggaran standar pengkodean, tetapi semua ini akan sia-sia jika kode tersebut tidak berfungsi dengan benar atau mengandung kesalahan runtime. Selain itu, aturan dari MISRA atau CERT biasanya hanya sebagian dari standar pengkodean yang diadopsi di perusahaan.



Analisis statis bukanlah obat mujarab



Standar tersebut menentukan tinjauan kode sistematis untuk menemukan cacat dalam kode dan menganalisis kode untuk standar pengkodean.



Alat analisis statis yang biasa digunakan untuk tujuan ini pandai menemukan kekurangan, tetapi alat tersebut tidak membuktikan bahwa kode sumber bebas dari kesalahan waktu proses. Dan banyak kesalahan yang terdeteksi oleh penganalisis statis sebenarnya adalah alat yang positif palsu. Alhasil, penggunaan alat-alat ini tidak banyak mengurangi waktu yang dihabiskan untuk memeriksa kode karena perlu memeriksa hasil pemeriksaan. Lebih buruk lagi, mereka mungkin tidak mendeteksi kesalahan runtime, yang tidak dapat diterima untuk aplikasi yang membutuhkan keandalan tinggi.



Verifikasi kode formal



Jadi, penganalisis statis tidak selalu dapat menangkap kesalahan waktu proses. Bagaimana mereka dapat dideteksi dan dihilangkan? Dalam hal ini, verifikasi formal kode sumber diperlukan.



Pertama-tama, Anda perlu memahami jenis hewan apa itu? Verifikasi formal adalah bukti kode bebas kesalahan menggunakan metode formal. Kedengarannya menakutkan, tapi nyatanya - ini seperti pembuktian dalil dari matan. Tidak ada keajaiban di sini. Metode ini berbeda dari analisis statis tradisional, karena menggunakan interpretasi abstrakdaripada heuristik. Ini memberi kita hal berikut: kita dapat membuktikan bahwa tidak ada error runtime tertentu dalam kode. Apa kesalahan ini? Ini semua adalah jenis overrun array, pembagian dengan nol, overflow integer, dan seterusnya. Kekejaman mereka terletak pada kenyataan bahwa kompilator akan mengumpulkan kode yang mengandung kesalahan seperti itu (karena kode tersebut benar secara sintaksis), tetapi ketika kode ini dijalankan, mereka akan muncul.



Mari kita lihat contohnya. Di bawah ini di spoiler adalah kode untuk pengontrol PI sederhana:



Lihat Kode
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);







Mari jalankan pengujian dengan Polyspace Bug Finder , penganalisis statis bersertifikat dan berkualitas, dan dapatkan hasil berikut:







Untuk kenyamanan, mari kita tabulasi hasilnya:



Lihat hasil






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





Sekarang mari kita verifikasi kode yang sama menggunakan alat verifikasi formal Polyspace Code Prover:





Hijau di hasil adalah kode yang telah terbukti bebas dari kesalahan runtime. Merah - kesalahan yang terbukti. Oranye - Alat kehabisan data. Hasil yang ditandai dengan warna hijau adalah yang paling menarik. Jika pada bagian kode tidak adanya kesalahan runtime telah terbukti, maka untuk bagian kode ini jumlah pengujian dapat dikurangi secara signifikan (misalnya, pengujian ketahanan tidak dapat lagi dilakukan) Dan sekarang, mari kita lihat tabel ringkasan kesalahan potensial dan terbukti:



Lihat hasil






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)







Tabel ini memberi tahu saya ini:



Ada error runtime di baris 93 yang dijamin akan terjadi. Peringatan lainnya memberi tahu saya bahwa saya salah mengonfigurasi verifikasi, atau saya perlu menulis kode keamanan atau mengatasinya dengan cara lain.



Tampaknya verifikasi formal sangat keren dan keseluruhan proyek harus diverifikasi secara tidak terkendali. Namun, seperti halnya instrumen apa pun, ada batasan, terutama terkait dengan waktu yang dihabiskan. Singkatnya, verifikasi formal lambat. Sangat lambat. Kinerja dibatasi oleh kompleksitas matematis dari interpretasi abstrak itu sendiri dan volume kode yang akan diverifikasi. Oleh karena itu, Anda tidak boleh mencoba memverifikasi kernel Linux dengan cepat. Semua proyek verifikasi di Polyspace dapat dibagi menjadi beberapa modul yang dapat diverifikasi secara independen satu sama lain, dan setiap modul memiliki konfigurasinya sendiri. Artinya, kami dapat menyesuaikan ketelitian verifikasi untuk setiap modul secara terpisah.





"Percaya" pada alat



Ketika Anda berurusan dengan standar industri seperti KT-178C atau GOST R ISO 26262, maka Anda terus-menerus menemukan hal-hal seperti "kepercayaan pada alat" atau "kualifikasi alat". Apa itu? Ini adalah proses di mana Anda menunjukkan bahwa hasil alat pengembangan atau pengujian yang digunakan dalam proyek dapat dipercaya dan kesalahannya didokumentasikan. Proses ini adalah topik untuk artikel terpisah, karena tidak semuanya jelas. Hal utama di sini adalah: alat yang digunakan dalam industri selalu disertai dengan serangkaian dokumen dan tes yang membantu dalam proses ini.



Hasil



Dengan contoh sederhana, kami melihat perbedaan antara analisis statis klasik dan verifikasi formal. Bisakah itu diterapkan di luar proyek yang membutuhkan kepatuhan terhadap standar industri? Ya, tentu saja kamu bisa. Anda bahkan dapat meminta versi trial di sini .



Ngomong-ngomong, kalau tertarik bisa bikin artikel tersendiri tentang sertifikasi instrumen. Tulis di komentar jika artikel seperti itu dibutuhkan.



All Articles