الأساليب الشكلية في هندسة البرمجيات
تطبق الأساليب الشكلية المنطق الرياضي على مواصفات البرمجيات وتطويرها والتحقق منها، مما يسمح بإثبات خصائص النظام بدلاً من مجرد اختبارها.
Definition
الأساليب الشكلية هي تقنيات قائمة على الرياضيات لتحديد وتطوير والتحقق من أنظمة البرمجيات، حيث يتم التعبير عن المواصفات بلغات شكلية ويتم إثبات الخصائص عن طريق البرهان أو الاستكشاف الشامل للحالات.
Scope
يغطي هذا الموضوع لغات المواصفات الشكلية مثل Z و B و TLA+؛ والدلالات البديهية ومنطق هوار (Hoare logic) للاستدلال حول صحة البرامج؛ والتحقق من النماذج (model checking) للتحقق من الأنظمة ذات الحالات المحدودة والمتزامنة؛ وإثبات النظريات ومساعدات الإثبات؛ واستخدام الأساليب الشكلية في البرمجيات الحساسة للسلامة والأمن.
Core questions
- كيف يمكن تحديد سلوك البرمجيات بشكل لا لبس فيه بلغة شكلية؟
- كيف يتم إثبات صحة البرنامج فيما يتعلق بالمواصفات؟
- كيف يتحقق التحقق من النماذج بشكل شامل من الأنظمة ذات الحالات المحدودة والمتزامنة؟
- أين تبرر تكاليف وفوائد الأساليب الشكلية استخدامها؟
Key theories
- منطق هوار والدلالات البديهية
- قدم هوار منطقًا للشروط المسبقة والشروط اللاحقة حيث يتم التعبير عن صحة بناءات البرنامج بواسطة البديهيات وقواعد الاستدلال، مما يوفر أساسًا لإثبات أن البرامج تلبي مواصفاتها.
- التحقق من النماذج
- يستكشف التحقق من النماذج تلقائيًا وبشكل شامل الحالات القابلة للوصول لنموذج ذي حالة محدودة للتحقق من خصائص المنطق الزمني، ويكشف عن الجمود والانتهاكات التي قد يفوتها الاختبار على الأرجح.
Clinical relevance
توفر الأساليب الشكلية أقوى ضمان متاح للصحة وتُطبق حيث يكون الفشل غير مقبول — في إلكترونيات الطيران، وإشارات السكك الحديدية، وبروتوكولات الأمان، والأجهزة — على الرغم من أن تكلفتها تحصرها بشكل رئيسي على المكونات الحيوية بدلاً من الأنظمة الكبيرة بأكملها.
Evidence & guidelines
توثق الدراسات الاستقصائية للممارسات الصناعية التطبيق الناجح للأساليب الشكلية في المجالات الحساسة للسلامة، وتدرك المعايير مثل DO-178C والمعايير المشتركة (Common Criteria) التقنيات الشكلية عند أعلى مستويات الضمان.
History
تأسس التحقق من البرامج على يد فلويد وهوار في أواخر الستينيات، وتم تطوير التحقق من النماذج بواسطة كلارك وإيمرسون وسيفاكيس في أوائل الثمانينيات (وحصلوا على جائزة تورنغ)، ومنذ ذلك الحين، أدخلت الأدوات ومساعدات الإثبات التحقق الشكلي في الاستخدام الصناعي للأنظمة الحيوية.
Debates
- قابلية التوسع وتكلفة الأساليب الشكلية
- يدور نقاش مستمر حول ما إذا كانت الأساليب الشكلية تتوسع لتشمل البرمجيات الصناعية الكبيرة اقتصاديًا؛ وقد أدت التطورات في الأتمتة والأساليب الشكلية الخفيفة إلى توسيع نطاق التطبيق، لكن التحقق الكامل من الأنظمة الكبيرة لا يزال مكلفًا.
Key figures
- C. A. R. Hoare
- Edsger Dijkstra
- Edmund Clarke
- Leslie Lamport
Related topics
Seminal works
- hoare1969
- clarke1999
- woodcock2009
Frequently asked questions
- هل تحل الأساليب الشكلية محل الاختبار؟
- بشكل عام لا. توفر الأساليب الشكلية ضمانات قوية حول نموذج أو مواصفات، لكن الافتراضات والبيئة والجوانب غير الممثلة في النموذج لا تزال تتطلب الاختبار؛ وفي الممارسة العملية، يكمل الاثنان بعضهما البعض، مع تركيز الأساليب الشكلية على الخصائص الأكثر أهمية.
- لماذا لا تستخدم الأساليب الشكلية في كل مكان؟
- إنها تتطلب خبرة وجهدًا متخصصين يصعب تبريرهما لمعظم البرمجيات، حيث يوفر الاختبار ثقة كافية بتكلفة أقل؛ تتركز الأساليب الشكلية حيث تكون عواقب الفشل وخيمة بما يكفي لتبرير الاستثمار.