PROFILPELAJAR.COM

في سياق أنظمة العتاد والبرمجيات ، فإن التحقق الشكلي هو إثبات أو دحض صحة الخوارزميات التي يقوم عليها النظام فيما يتعلق بمواصفات أو خواص شكلية معينة، باستخدام طرق شكلية رياضية .^[1]

يمكن أن يكون التحقق الشكلي مفيدًا في إثبات صحة الأنظمة مثل: مواثيق التشفير ، والدوائر المنطقية ، والدوائر الرقمية ذات الذاكرة الداخلية ، والبرامج.

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

المنهجيات

أحد المنهجيات هو فحص النموذج ، والذي يتكون من استكشاف شامل منظم للنموذج الرياضي (هذا ممكن للنماذج المحدودة ، ولكن أيضًا لبعض النماذج اللانهائية حيث يمكن تمثيل مجموعات لا نهائية من الحالات بشكل فعال باستخدام التجريد أو الاستفادة من التماثل). عادة ، يتكون هذا من استكشاف جميع الحالات في النموذج ، باستخدام تقنيات تجريد ذكية ومتخصصة للنظر في مجموعات كاملة من الحالات في عملية واحدة وتقليل وقت الحوسبة. تشمل تقنيات التنفيذ: تعداد فضاء الحالة ، وتعداد مساحة الحالة الرمزية ، والتفسير المجرد ، والمحاكاة الرمزية ، وصقل التجريد. الخصائص المراد التحقق منها غالبًا ما يتم وصفها في المنطقيات الزمنية ، مثل المنطق الزمني الخطي و لغة مواصفات الخاصية ، تأكيدات سيستم فيريلوج ، ^[3] أو منطق الشجرة الحسابي. الميزة الكبرى لفحص النموذج هي أنه غالبًا ما يكون آليًا بالكامل؛ عيبه الأساسي هو أنه لا يناسب الأنظمة كبيرة الحجم حيث تقتصر النماذج الرمزية عادةً على بضع مئات من بتات الحالة فقط، بينما يتطلب تعداد فضاء الحالة الصريح أن يكون حجم الفضاء صغير نسبيًا.

نهج آخر هو التحقق الاستنتاجي. وهو يتألف من إنشاء مجموعة من التزامات الإثبات الرياضي من النظام ومواصفاته، وتنفيذ هذه الالتزامات باستخدام أي من مساعدي الإثبات (المبرهنات) ( مثل HOL ، أو ACL2 ، أو Isabelle ، أو Coq ، أو PVS ) ، أو المبرهنات الآلية ، بما في ذلك على وجه الخصوص حلالات نظرية الإمكانية. هذا النهج له عيوب أنه قد يتطلب من المستخدم أن يفهم بالتفصيل سبب عمل النظام بشكل صحيح ، ونقل هذه المعلومات إلى نظام التحقق ، إما في شكل سلسلة من النظريات التي سيتم إثباتها أو في شكل مواصفات ( الثوابت والشروط المسبقة والظروف اللاحقة) لمكونات النظام (مثل الوظائف أو الإجراءات) وربما المكونات الفرعية (مثل الحلقات أو هياكل البيانات).

برمجة

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

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

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

التحقق والمصادقة

التحقق هو أحد جوانب اختبار ملاءمة المنتج للغرض. والمصادقة هي جانب مكمل أيضًا

المصادقة : "هل نحاول صنع الشيء الصحيح؟" ، أي هل المنتج محدد لاحتياجات المستخدم الفعلية؟
التحقق : "هل صنعنا ما كنا نحاول صنعه؟" أي هل المنتج مطابق للمواصفات؟

تتكون عملية التحقق من جوانب ثابتة / هيكلية وديناميكية / سلوكية. على سبيل المثال ، بالنسبة لمنتج برمجي ، يمكن للمرء فحص كود المصدر (ثابت) وتشغيله مقابل حالات اختبار محددة (ديناميكية).

بينما المصادقة تُجرى بشكل ديناميكي فقط ، على سبيل المثال ، يتم اختبار المنتج من خلال وضعه من خلال استخدامات قياسية وغير قياسية ("هل يلبي جميع حالات الاستخدام بشكل مرضي؟" ).

الإصلاح الآلي للبرنامج

يتم إصلاح البرنامج فيما يتعلق بـ المستشار ، بما في ذلك الوظيفة المطلوبة للبرنامج والتي يتم استخدامها للتحقق من الإصلاح الذي تم إنشاؤه. مثال بسيط هو منصة الاختبار — تحدد أزواج الإدخال / الإخراج وظائف البرنامج. يتم استخدام مجموعة متنوعة من التقنيات ، وعلى الأخص استخدام حلّالّات نظريات الإمكانية والبرمجة الجينية ، ^[4] باستخدام الحوسبة التطورية لتوليد وتقييم المرشحين المحتملين للإصلاحات. الطريقة الأولى حتمية ، بينما الطريقة الأخيرة عشوائية.

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

الاستخدام الصناعي

يزيد النمو في تعقيد التصاميم من أهمية تقنيات التحقق الشكلية في صناعة العتاد .^[5]^[6] في الوقت الحاضر ، يتم استخدام التحقق الشكلي من قبل معظم أو كل شركات الأجهزة الرائدة ، ^[7] ولكن استخدامها في صناعة البرمجيات لا يزال ضعيفًا. هذا يمكن أن يعزى إلى الحاجة المتزايدة في صناعة العتاد، حيث الأخطاء لها أهمية تجارية أكبر. بسبب التفاعلات الدقيقة المحتملة بين المكونات ، من الصعب بشكل متزايد ممارسة مجموعة واقعية من الاحتمالات عن طريق المحاكاة. تخضع الجوانب المهمة لتصميم الأجهزة لطرق الإثبات الآلي ، مما يجعل التحقق الشكلي أسهل وأكثر إنتاجية.^[8]

اعتبارًا من 2011^[تحديث], تم التحقق شكليًا من: نواة نسيتا المحمية ونظام أوسيك فدكس الفوري وأيضًا نظام انتجرتي

اعتبارًا من عام 2017 ، تم تطبيق التحقق الشكلي على تصميم شبكات الكمبيوتر الكبيرة من خلال نموذج رياضي للشبكة ، ^[9] وكجزء من فئة تكنولوجيا الشبكة الجديدة ، الشبكات القائمة على النوايا.^[10] بائعي برامج الشبكات الذين يقدمون حلول تحقق شكلية يشملون سيسكو و شبكات فوروارد ^[11]^[12] وأنظمة فيريفلو.^[13]

توفر لغة البرمجة سبارك مجموعة أدوات تمكن من تطوير البرامج مع التحقق الشكلي وتستخدم في العديد من الأنظمة عالية التكامل .

مترجم CompCert C هو مترجم C تم التحقق منه شكليًا وينفذ غالبية ISO C.^[14]^[15]

أنظر أيضا

المبرهن الآلي
فحص النموذج
قائمة أدوات فحص النموذج
فحص التكافؤ الشكلي
مدقق إثبات
لغة مواصفات الخاصية
تحليل الكود الثابت
المنطق الزمني في التحقق من الحالة المحدودة
التحقق من صحة ما بعد التصنيع
التحقق الذكي
التحقق من وقت التشغيل

مراجع

^ Sanghavi، Alok (21 مايو 2010). "What is formal verification?". EE Times Asia.
^ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013 نسخة محفوظة 2022-06-21 على موقع واي باك مشين.
^ Cohen، Ben؛ Venkataramanan، Srinivasan؛ Kumari، Ajeetha؛ Piper، Lisa (2015). SystemVerilog Assertions Handbook (ط. 4th). CreateSpace Independent Publishing Platform. ISBN:978-1518681448.
^ Le Goues، Claire؛ Nguyen، ThanhVu؛ Forrest، Stephanie؛ Weimer، Westley (يناير 2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Transactions on Software Engineering. ج. 38 ع. 1: 54–72. DOI:10.1109/TSE.2011.104. مؤرشف من الأصل في 2020-03-16.
^ Harrison، J. (2003). "Formal verification at Intel". 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. ص. 45–54. DOI:10.1109/LICS.2003.1210044. ISBN:978-0-7695-1884-8.
^ Formal verification of a real-time hardware design. Portal.acm.org (June 27, 1983). Retrieved on April 30, 2011. نسخة محفوظة 2023-03-26 على موقع واي باك مشين.
^ "Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015. مؤرشف من الأصل في 2021-12-04.
^ "Formal Verification in Industry" (PDF). مؤرشف من الأصل (PDF) في 2022-02-01. اطلع عليه بتاريخ 2012-09-20.
^ Scroxton، Alex. "For Cisco, intent-based networking heralds future tech demands". Computer Weekly. مؤرشف من الأصل في 2022-12-09. اطلع عليه بتاريخ 2018-02-12.
^ Lerner، Andrew. "Intent-based networking". Gartner. مؤرشف من الأصل في 2023-03-31. اطلع عليه بتاريخ 2018-02-12.
^ "Forward Networks: Accelerating and De-risking Network Operations". Insights Success. مؤرشف من الأصل في 2022-12-08. اطلع عليه بتاريخ 2018-02-12.
^ "Getting Grounded in Intent=based Networking" (PDF). NetworkWorld. مؤرشف من الأصل (PDF) في 2022-01-07. اطلع عليه بتاريخ 2018-02-12.
^ "Veriflow Systems". Bloomberg. مؤرشف من الأصل في 2020-03-31. اطلع عليه بتاريخ 2018-02-12.
^ "CompCert - The CompCert C compiler". compcert.org. مؤرشف من الأصل في 2023-01-10. اطلع عليه بتاريخ 2023-02-22.
^ Barrière، Aurèle؛ Blazy، Sandrine؛ Pichardie، David (9 يناير 2023). "Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler". Proceedings of the ACM on Programming Languages. ج. 7 ع. POPL: 249–277. DOI:10.1145/3571202. ISSN:2475-1421. مؤرشف من الأصل في 2023-02-22.