تحقق شكلي

في علم الحاسوب النظري، التحقق الشكلي هو برهان أو إبطال صحة خوارزمية التي تُسيِّر نظاماً ما وفقاً لعدد من المواصفات 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] تحاول أتمتة عملية البرهان بشكل كامل.

 انظر أيضاً

ابحث عن verifiability في
قاموس المعرفة.

• Automated theorem proving
• Formal equivalence checking
• LURCH
• Model checking
• Proof checker
• Property Specification Language
• Selected formal verification bibliography
• Static code analysis
• Temporal logic in finite-state verification
• Post silicon validation
• Intelligent verification
• Verification and Validation
• Runtime verification