تحقق شكلي

في فهم الحاسوب النظري، التحقق الشكلي هوبرهان أوإبطال صحة خوارزمية التي تُسيِّر نظاماً ما وفقاً لعدد من المواصفات formal specification أوخصائص شكلية محددة، باستخدام المناهج الشكلية للرياضيات. ^{[بحاجة لمصدر]}

الاستخدام

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

عادة ما يتم البرهان باستخدام برهان شكلي على نموذج رياضي مجرد للنظام. من الأمثلة على النماذج الرياضية المستخدمة في نمذجة النظم: finite state machines، labelled transition systems، Petri nets، timed automata، hybrid automata، process algebra، formal semantics of programming languages such as operational semantics، denotational semantics، axiomatic semantics and Hoare logic.^[]

مقاربات التحقق الشكلي

هناك مقاربتان للتحقق الشكلي. ^{[بحاجة لمصدر]}

المقاربة الأولى والتشكيل الأول هوتفقد النموذج model checking، الذي يتضمن استكشافاً شاملاً وممنهجاً للنموذج الرياضي (وهذا ممكن للنماذج المحدودة ولبعض النماذج اللامنتهية التي يمكن تمثيل عناصرها اللامنتهية بشكل فعّال). هذا يتضمن غالباً استكشاف ورصد جميع الحالات والانتنطقات التي تحدث في النموذج من خلال تقنيات تجريد ذكية ومحددة النطاق تستطيع حتى تضم جميع استيعاب جميع مجموعات الحالات في عملية واحدة واختزال الوقت اللازم للحساب.

وتضم تقانات التطبيق state space enumeration، symbolic state space enumeration، abstract interpretation، symbolic simulation، abstraction refinement. The properties to be verified are often described in temporal logics، such as linear temporal logic (LTL) or computational tree logic (CTL).

أما المقاربة الثانية فهي الاستدلال المنطقي. تتضمن استخدام نسخ شكلية (صورية) من التفكير الرياضي على النظام، من خلال استخدام برمجيات برهان المبرهنات مثل HOL theorem prover، وبرنامج ACL2، Isabelle، or وبرنامج Coq.غالباً ما تكون هذه البرمجيات آلية بشكل جزئية، بينماقد يكون الموجه الأساسي هوفهم المستخدم للنظام المراد التحقق من صحته. توجد أدوات حديثة مثل المطور المثالي Perfect Developer و[[ArC] تحاول أتمتة عملية البرهان بشكل كامل.