تحليل كود الأنظمة ذات الموثوقية المتزايدة

مرحبا هبر! في هذه المقالة ، أود التحدث عن موضوع تمت مناقشته قليلاً وهو تحليل الكود للأنظمة عالية الموثوقية. هناك العديد من المقالات حول Habré حول ماهية التحليل الثابت الجيد ، لكن في هذه المقالة أود أن أتحدث عن ماهية التحقق الرسمي من الكود ، وأشرح أيضًا مخاطر الاستخدام غير المدروس للمحللات الثابتة ومعايير الترميز.



كان هناك الكثير من الجدل حول كيفية إنشاء برامج ذات موثوقية متزايدة ، ونوقش المنهجيات والأساليب لتنظيم التطوير والأدوات. ولكن من بين كل هذه المناقشات ، ما ضاع هو أن تطوير البرمجيات هو عملية ، ومدروسة بشكل جيد وصياغتها. وإذا نظرت إلى هذه العملية ، ستلاحظ أن هذه العملية لا تركز فقط على كيفية كتابة / إنشاء الكود ، ولكن على كيفية التحقق من هذا الرمز. الأهم من ذلك ، تتطلب التنمية استخدام الأدوات التي يمكنك "الوثوق بها".



انتهت هذه الجولة القصيرة ، ودعونا نرى كيف ثبت أن الشفرة موثوقة. أولاً ، تحتاج إلى فهم خصائص الكود الذي يلبي متطلبات الموثوقية. يبدو مصطلح "موثوقية الكود" غامضًا ومتناقضًا إلى حد ما. لذلك ، أفضل عدم اختراع أي شيء ، وعند تقييم موثوقية الكود ، فإنني أسترشد بمعايير الصناعة ، على سبيل المثال ، GOST R ISO 26262 أو KT-178C. الصياغة فيها مختلفة ، لكن الفكرة هي نفسها: تم تطوير كود موثوق وفقًا لمعيار واحد (ما يسمى بمعيار الترميز ) وتقليل عدد أخطاء وقت التشغيل فيه. ومع ذلك ، فإن كل شيء ليس بهذه البساطة هنا - حيث تنص المعايير على المواقف التي يكون فيها ، على سبيل المثال ، الامتثال لمعيار الترميز غير ممكن ويحتاج هذا الانحراف إلى التوثيق



مستنقع خطير ميسرة وما شابه



تهدف معايير الترميز إلى تقييد استخدام تراكيب لغة البرمجة التي يمكن أن تكون خطرة. من الناحية النظرية ، يجب أن يؤدي هذا إلى تحسين جودة الكود ، أليس كذلك؟ نعم ، هذا يضمن جودة الكود ، لكن من المهم دائمًا تذكر أن الامتثال بنسبة 100٪ لقواعد الترميز ليس غاية في حد ذاته. إذا كان الرمز متوافقًا بنسبة 100٪ مع قواعد بعض MISRA ، فهذا لا يعني على الإطلاق أنه جيد وصحيح. يمكنك قضاء الكثير من الوقت في إعادة البناء ، وإزالة انتهاكات معيار الترميز ، ولكن كل هذا سيضيع إذا انتهى الكود بالعمل بشكل غير صحيح أو يحتوي على أخطاء في وقت التشغيل. علاوة على ذلك ، فإن القواعد من 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);







دعنا نجري الاختبار باستخدام 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 kernel. يمكن تقسيم جميع مشاريع التحقق في Polyspace إلى وحدات يمكن التحقق منها بشكل مستقل عن بعضها البعض ، ولكل وحدة تكوينها الخاص. وهذا يعني أنه يمكننا ضبط دقة التحقق لكل وحدة على حدة.





"الثقة" في الأدوات



عندما تتعامل مع معايير الصناعة مثل KT-178C أو GOST R ISO 26262 ، فإنك تصادف باستمرار أشياء مثل "الثقة في الأداة" أو "تأهيل الأداة". ما هذا؟ هذه هي العملية التي تُظهر فيها أن نتائج أدوات التطوير أو الاختبار التي تم استخدامها في المشروع يمكن الوثوق بها وتوثيق أخطائها. هذه العملية موضوع لمقال منفصل ، لأنه ليس كل شيء واضح. الشيء الرئيسي هنا هو أن الأدوات المستخدمة في الصناعة تأتي دائمًا مع مجموعة من المستندات والاختبارات التي تساعد في هذه العملية.



النتيجة



بمثال بسيط ، نظرنا إلى الفرق بين التحليل الساكن الكلاسيكي والتحقق الرسمي. هل يمكن تطبيقه خارج المشاريع التي تتطلب الالتزام بمعايير الصناعة؟ نعم بالطبع يمكنك ذالك. يمكنك حتى أن تطلب نسخة تجريبية هنا .



بالمناسبة ، إذا كنت مهتمًا ، يمكنك عمل مقال منفصل حول شهادة الجهاز. اكتب في التعليقات إذا كانت هناك حاجة لمثل هذا المقال.



All Articles