علوم البرمجة

يمكننا كتابة برمجيات خالية من الأخطاء…إذاً، لماذا لا نقوم بذلك؟

أشار عالم الحاسوب الهولندي الكبير Edsger W Dijkstra أن الاختبار يبين وجود الأخطاء وليس غيابها. في الحقيقة، إن الطريقة الحاسمة الوحيدة لإثبات صحة البرمجيات وخلوها من الأخطاء هي من خلال الرياضيات.

لقد كان من المتعارف عليه أنه من الصعب الوصول إلى برمجيات صحيحة. منذ أن نظم Friedrich L Bauer المؤتمر الأول عن هندسة البرمجيات في عام 1968، اخترع علماء الحاسوب منهجيات لبناء وتوجيه تطوير البرمجيات. تستخدم إحدى هذه المنهجيات، والتي تدعى أحياناً هندسة البرمجيات القوية أو في الغالب المنهجيات الأكثر رسمية، الرياضيات للتأكد من أن البرمجيات خالية من الخطأ.

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

هندسة البرمجيات الرسمية:
لطالما كانت بريطانيا متخصصة في المنهجيات الرسمية. تم منح اثنين من علماء الحاسوب
توني هاور ( أوكسفورد 1977 – ، مركز أبحاث مايكروسوفت) والراحل روبن ميلنر (إدنبرة 1973-1995 ، كامبريدج 1995-2001) جوائز تورينج – التي تمثل جائزة نوبل للحوسبة – على أعمالهم في المنهجيات الرسمية.
يعد عالم الحاسوب كليف بي. جونز أحد مخترعي منهجية فيينا للتطوير. وبينما كان يعمل لدى IBM في فيينا، ومختبر جامعة أوكسفورد للحوسبة و IBM بريطانيا، بقيادة توني هاور، فازا معا بجائزة الملكة للإنجاز التقني لعملهم على جعل برمجيات (IBM’s CICS ) (أنظمة التحكم بمعلومات الزبون الخاصة بـ IBM) رسمية. وقامــا من ناحية أخرى خلال سير العمل بتطوير”ترميز Z” الذي أصبح أحد المنهجيات الرسمية الأساسية.
تستلزم عملية المنهجيات الرسمية وصف ما يفترض على البرنامج فعله باستخدام الرموز الرياضية والمنطقية، ومن ثم استخدام البراهين المنطقية والرياضية للتأكيد على أن البرنامج يقوم بما يجب عليه بالفعل. على سبيل المثال، الصيغة المنطقية التالية لـ هاور التي تصف عمل البرنامج تظهر
كيف تقوم المنهجيات الرسمية باختزال الكتابة البرمجية إلى شيء مختصر بحيث لا يمكن اختزاله أكثر.

صيغة منطق Hoare:

1-itspossiblet
إذا بدأ برنامج S في حالة يحقق فيها الشرط P فإنه يأخذنا إلى حالة يحقق فيها الشرط Q، وكان هناك برنامج T يأخذنا من Q إلى R ، عندها يُنفَّذ S ثم يأخذنا T من P إلى R .
دُرِّست المنهجيات الرسمية في أغلب الجامعات البريطانية منذ منتصف الثمانينات، وشهدت استخداماً كبيراً من قبل المصانع في أنظمة السلامة الحرجة. كما وصلت التحسينات الأخيرة إلى النقطة حيث يمكن لقدرة المنهجيات الرسمية على فحص وتأكيد صحة الكود أن تطبق عند القياس مع أدوات آلية ضخمة.

فهمت الحكومة الرسالة:
على كل حال، هل هناك أي دافع لمشاهدة هذه المنهجيات تستخدم بشكل أوسع؟
عندما أخذت لجنة الشؤون الداخلية الأدلة في تحقيقها في حال الجريمة الإلكترونية في نيسان 2013، قام البروفيسور جيم نورتون، الرئيس السابق لجمعية الحاسوب البريطانية، بإخبار اللجنة التالي:
“نحن بحاجة برمجيات أفضل، ونعلم كيف بإمكاننا كتابة برمجيات أفضل بكثير مما نفعل الآن في تطبيقاتنا الحالية. إننا لا نستخدم المنهجيات الرياضية الرسمية المتاحة، والموجودة لدينا منذ 40 عاماً، لإنتاج برمجيات أفضل.”

بناءاً على أدلة نورتون، طرحت اللجنة في توصيات رقم 32 ” أن تصبح برمجيات البنية التحتية الرئيسية آمنة بصورة مبرهنة، من خلال استخدام المنهجيات الرياضية للكتابة البرمجية.”

بعد شهرين في أيار، أخذت لجنة العلوم والتكنولوجيا الأدلة إلى برنامج رقمي افتراضياً للخدمات العامة المسلمة عبر الانترنت. كان الدكتور مارتن توماس ، مؤسس براكسيس، أحد أكثر الشركات البارزة استخداماً للمنهجيات الرسمية من أجل تطوير أنظمة السلامة الحرجة، أحد الخبراء المدعوين. وقد سُئِل عن كيفية تحقيق المراحل المطلوبة من الأمان، فـأجاب:
إن الكميات الضخمة من التجريب لن تعطيك درجة عالية من الوثوقية بأن الأشياء صحيحة أو تملك الخواص التي تتوقعها. لابد من القيام بذلك من خلال التحليل. هذا يعني أن البرمجيات يجب أن تكتب بطريقة يمكن تحليلها، وهذا تغير كبير عن الطريقة التي يعمل بها المصنع الآن.

أرسلت اللجنة رسالة صريحة إلى سكرتير الحكومة فرانسيس ماود لتسأله فيما إذا كانت الحكومة ” واثقة أن البرمجيات المطورة تطابق أعلى المعايير الهندسية”.

البرمجيات الموثوقة هي الإجابة:
ذكرت الحكومة في ردها على تقرير الجريمة الإلكترونية في تشرين الأول 2013:
إن الحكومة تدعم توصية لجنة الشؤون الداخلية رقم 32. لهذه الغاية قامت الحكومة باستثمار مبادرة البرمجيات الموثوقة، مبادرة مشتركة عامة/خاصة لوضع توجيهات ومعلومات عن تطوير البرمجيات الموثوقة والآمنة.

يبدو هذا الأمر مشجعاً. لم يتم نشر رد ماود إلى لجنة التكنولوجيا والعلوم الذي ذكره ذلك الشهر حتى تشرين الأول 2014، إلا أنه ذكر الشيء ذاته.
لذا قد يعتقد أحدهم أنه تم وضع الـ TSI خصيصاً لمعالجة توصية اللجنة، لكن فيما بعد تبين أن الأمر ليس كذلك.
تم تأسيس الـ TSI عام 2011، تجاوباً مع مخاوف الحكومة من الأمان عبر الانترنت. وقد انتهت مرحلة “بدء العمل” عليها، والتي تم رسمها من الخبرة الأكاديمية للبرمجيات الموثوقة في آب 2014، بالتحضير للدليل المعنون لأطر برمجيات الأمان الموثوقة، المتاحة كمعيار PAS 754:2014 لمعهد المعايير البريطانية.

إنها مجموعة قيمة جداً من تطبيقات هندسة البرمجيات المبنية على المخاطر (وبالمناسبة، التطبيقات الموصوفة في دليل خدمة رقمي افتراضياً ليست ذكية وليست مكررة ولا تتمحور حول المستخدم). لكن حتى الآن لم تعطى المنهجيات الرسمية أي دور في هذا. وقد قدم مدير TSI إيان براينت المنهجيات الرسمية في الخطاب الرئيسي لمؤتمر BSC لمعايير جودة البرمجيات عام 2012 بتنويه عابر على أنها ” الطرق التقنية لإدارة المخاطر”.
وبالتالي، فقد نُصحت الحكومة البريطانية مرتين باستخدام الرياضيات والمنهجيات الرسمية لضمان صحة البرمجيات، لكن إعلانها لمرتين أن TSI هي أداتها للقيام بذلك يدل على أنه لم يحصل أي شيء. لذلك فمرات اختبار الصحة البرامج ستسمر حتى تصل رسالة Dijkstra

ترجمة وإعداد: Ghalia Turki

المصدر: phys.org

Mhd Jafar Mourtada

طالب هندسة طبية في جامعة دمشق

مقالات ذات صلة

زر الذهاب إلى الأعلى