الأساليب الرسمية

📅 آخر تحديث: ١ أغسطس ٢٠٢٦
✍️ نُشر في: ١ أغسطس ٢٠٢٦
📷 يحتوي على 2 صور
الموسوعة الحرة

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

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

الاستخدامات

يمكن تطبيق الأساليب الرسمية في نقاط مختلفة خلال عملية التطوير .

مواصفة

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

بدلاً من ذلك، قد تكون مرحلة تحديد المواصفات هي المرحلة الوحيدة التي تُستخدم فيها الأساليب الرسمية. فمن خلال كتابة المواصفات، يمكن اكتشاف أوجه الغموض في المتطلبات غير الرسمية وحلها. إضافةً إلى ذلك، يمكن للمهندسين استخدام المواصفات الرسمية كمرجع لتوجيه عمليات التطوير الخاصة بهم. [ 4 ]

لطالما لوحظت الحاجة إلى أنظمة مواصفات رسمية. في تقرير ALGOL 58 ، [ 5 ] قدم جون باكوس تدوينًا رسميًا لوصف بناء جملة لغة البرمجة ، سُمي لاحقًا بصيغة باكوس العادية ، ثم أُعيد تسميته بصيغة باكوس-ناور (BNF). [ 6 ] وكتب باكوس أيضًا أن الوصف الرسمي لمعنى برامج ALGOL الصحيحة نحويًا لم يكتمل في الوقت المناسب لإدراجه في التقرير، مصرحًا بأنه "سيُدرج في ورقة بحثية لاحقة". ومع ذلك، لم تُنشر أي ورقة بحثية تصف الدلالات الرسمية. [ 7 ]

توليف

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

تَحَقّق

التحقق الرسمي هو استخدام أدوات البرمجيات لإثبات خصائص المواصفات الرسمية، أو لإثبات أن النموذج الرسمي لتنفيذ النظام يفي بمواصفاته.

بمجرد وضع مواصفات رسمية، يمكن استخدام هذه المواصفات كأساس لإثبات خصائص المواصفات، وبالتالي، خصائص تنفيذ النظام.

التحقق من الموافقة

التحقق بالتوقيع هو استخدام أداة تحقق رسمية موثوقة للغاية. يمكن لهذه الأداة أن تحل محل أساليب التحقق التقليدية (بل قد تكون معتمدة). [ 9 ]

إثبات موجه من قبل البشر

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

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

التدقيق الآلي

في المقابل، يتزايد الاهتمام بإنتاج براهين صحة هذه الأنظمة بوسائل آلية. وتنقسم التقنيات الآلية إلى ثلاث فئات عامة:

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

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

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

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

تتمثل السمة الرئيسية لمنهج التفسير المجرد في أنه يوفر تحليلاً دقيقاً، أي أنه لا يُنتج نتائج سلبية خاطئة. علاوة على ذلك، يتميز هذا المنهج بقابلية التوسع بكفاءة، وذلك من خلال ضبط المجال المجرد الذي يمثل الخاصية المراد تحليلها، وتطبيق عوامل التوسيع [ 10 ] لتحقيق تقارب سريع.

التقنيات

تشمل الأساليب الرسمية عدداً من التقنيات المختلفة.

لغات المواصفات

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

مخططات القرار الثنائي

مخطط القرار الثنائي هو بنية بيانات تمثل دالة منطقية . [ 12 ] إذا كانت الصيغة المنطقيةP{\displaystyle {\mathcal {P}}}إذا كان تنفيذ البرنامج متوافقًا مع المواصفات، فيمكن استخدام مخطط القرار الثنائي لتحديد ما إذا كانP{\displaystyle {\mathcal {P}}}هي عبارة صحيحة تلقائياً؛ أي أنها تُقيّم دائماً إلى القيمة TRUE. إذا كان الأمر كذلك، فإن البرنامج يتوافق دائماً مع المواصفات. [ 13 ]

حلول SAT

برنامج حل مشكلة SAT هو برنامج قادر على حل مشكلة إرضاء العبارات المنطقية ، وهي مشكلة إيجاد تعيين للمتغيرات يجعل صيغة منطقية معينة صحيحة.P{\displaystyle {\mathcal {P}}}يُعبّر عن أن تنفيذًا محددًا لبرنامج ما يتوافق مع المواصفات، ثم يتم تحديد ذلك.¬P{\displaystyle \neg {\mathcal {P}}}إن عدم إمكانية تحقيق الشرط يعادل تحديد أن جميع عمليات التنفيذ تتوافق مع المواصفات. تُستخدم خوارزميات حل مشكلة SAT غالبًا في التحقق من النماذج المحدودة، ولكن يمكن استخدامها أيضًا في التحقق من النماذج غير المحدودة. [ 14 ]

التطبيقات

تُطبَّق الأساليب الرسمية في مجالاتٍ مختلفة من الأجهزة والبرمجيات، بما في ذلك أجهزة التوجيه ، ومحولات الإيثرنت ، وبروتوكولات التوجيه ، وتطبيقات الأمان، ونوى أنظمة التشغيل المصغّرة مثل seL4 . وهناك أمثلة عديدة استُخدمت فيها هذه الأساليب للتحقق من وظائف الأجهزة والبرمجيات المستخدمة في مراكز البيانات . استخدمت شركة IBM برنامج ACL2 ، وهو برنامج لإثبات النظريات، في عملية تطوير معالج AMD x86. وتستخدم شركة Intel هذه الأساليب للتحقق من أجهزتها وبرامجها الثابتة (البرمجيات الدائمة المُبرمجة في ذاكرة للقراءة فقط ) . استخدم مركز Dansk Datamatik Center الأساليب الرسمية في ثمانينيات القرن الماضي لتطوير نظام مُترجم للغة البرمجة Ada ، والذي أصبح فيما بعد منتجًا تجاريًا ناجحًا استمر لسنوات طويلة. [ 15 ] [ 16 ]

هناك العديد من مشاريع ناسا الأخرى التي تُطبّق فيها الأساليب الرسمية، مثل نظام النقل الجوي من الجيل التالي ، ودمج أنظمة الطائرات بدون طيار في نظام المجال الجوي الوطني، [ 17 ] ونظام حل النزاعات والكشف المنسق المحمول جواً (ACCoRD). [ 18 ] كما تُستخدم طريقة B مع Atelier B ، [ 19 ] لتطوير أنظمة السلامة الآلية لمختلف خطوط المترو التي أنشأتها شركتا ألستوم وسيمنز في جميع أنحاء العالم ، وكذلك للحصول على شهادة المعايير المشتركة وتطوير نماذج الأنظمة من قِبل شركتي ATMEL و STMicroelectronics .

يُستخدم التحقق الرسمي بكثرة في مجال الأجهزة من قِبل معظم موردي الأجهزة المعروفين، مثل IBM و Intel وAMD. وقد استخدمت Intel أساليب رسمية للتحقق من عمل منتجاتها في العديد من مجالات الأجهزة، مثل التحقق المُعَلم من بروتوكول ذاكرة التخزين المؤقت المتماسكة [ 20 ] ، والتحقق من صحة محرك تنفيذ معالج Intel Core i7 [ 21 ] (باستخدام إثبات النظريات، ومخططات القرار الثنائية ، والتقييم الرمزي)، وتحسين بنية Intel IA-64 باستخدام مُثبت النظريات HOL light [ 22 ] ، والتحقق من وحدة تحكم إيثرنت جيجابت ثنائية المنافذ عالية الأداء مع دعم بروتوكول PCI Express وتقنية إدارة Intel المتقدمة باستخدام Cadence [ 23 ] . وبالمثل، استخدمت IBM أساليب رسمية في التحقق من بوابات الطاقة [ 24 ] ، والسجلات [ 25 ] ، والتحقق الوظيفي من معالج IBM Power7 [ 26 ] .

في تطوير البرمجيات

في مجال تطوير البرمجيات ، تُعدّ الأساليب الرسمية مناهج رياضية لحل مشكلات البرمجيات (والمكونات المادية) على مستويات المتطلبات والمواصفات والتصميم. ويُرجّح تطبيق هذه الأساليب على البرمجيات والأنظمة بالغة الأهمية من حيث السلامة أو الأمن، مثل برمجيات إلكترونيات الطيران . وتسمح معايير ضمان سلامة البرمجيات، مثل DO-178C، باستخدام الأساليب الرسمية من خلال التكميل، بينما تُلزم معايير التقييم المشتركة باستخدامها في أعلى مستويات التصنيف.

بالنسبة للبرمجيات التسلسلية، تشمل أمثلة الأساليب الرسمية طريقة B ، ولغات المواصفات المستخدمة في إثبات النظريات الآلي ، و RAISE ، ورمز Z.

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

لقد سمحت لغة قيود الكائنات (والتخصصات مثل لغة نمذجة جافا ) بتحديد الأنظمة الموجهة للكائنات بشكل رسمي، إن لم يكن بالضرورة التحقق منها بشكل رسمي.

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

يتمثل أحد الأساليب الرسمية في تطوير البرمجيات في كتابة المواصفات بلغة منطقية معينة - عادةً ما تكون صيغة من صيغ منطق الرتبة الأولى - ثم تنفيذ هذا المنطق مباشرةً كما لو كان برنامجًا. تُعد لغة OWL ، القائمة على منطق الوصف ، مثالًا على ذلك. كما يجري العمل على ربط نسخة من اللغة الإنجليزية (أو أي لغة طبيعية أخرى) تلقائيًا بالمنطق والعكس، بالإضافة إلى تنفيذ المنطق مباشرةً. ومن الأمثلة على ذلك Attempto Controlled English وInternet Business Logic، اللذان لا يسعيان إلى التحكم في المفردات أو بناء الجملة. ومن سمات الأنظمة التي تدعم الربط ثنائي الاتجاه بين اللغة الإنجليزية والمنطق والتنفيذ المباشر للمنطق، قدرتها على شرح نتائجها باللغة الإنجليزية، على مستوى الأعمال أو المستوى العلمي.

الأساليب شبه الرسمية

الأساليب شبه الرسمية هي أساليب ولغات رسمية لا تُعتبر "رسمية" بالكامل. وهي تؤجل مهمة إكمال الدلالات إلى مرحلة لاحقة، والتي يتم إنجازها إما عن طريق التفسير البشري أو عن طريق التفسير من خلال برامج مثل مولدات التعليمات البرمجية أو حالات الاختبار . [ 27 ]

يعتقد بعض الممارسين أن مجتمع الأساليب الرسمية قد بالغ في التركيز على الصياغة الرسمية الكاملة للمواصفات أو التصميم. [ 28 ] [ 29 ] ويجادلون بأن قدرة اللغات المستخدمة على التعبير ، بالإضافة إلى تعقيد الأنظمة التي يتم نمذجتها، تجعل الصياغة الرسمية الكاملة مهمة صعبة ومكلفة. وكبديل لذلك، تم اقتراح العديد من الأساليب الرسمية الخفيفة التي تركز على المواصفات الجزئية والتطبيق الموجه. ومن أمثلة هذا النهج الخفيف للأساليب الرسمية: تدوين نمذجة الكائنات Alloy ، [ 30 ] وتوليف ديني لبعض جوانب تدوين Z مع التطوير القائم على حالات الاستخدام ، [ 31 ] وأدوات CSK VDM . [ 32 ]

الأساليب والرموز الرسمية

تتوفر مجموعة متنوعة من الأساليب والرموز الرسمية.

لغات المواصفات

مدققو النماذج

  • ESBMC [ 33 ]
  • فيزبي [ 34 ]
  • مجموعة أدوات التحليل الثابت لبرنامج MALPAS – أداة فحص نماذج صناعية قوية تُستخدم للتحقق الرسمي من الأنظمة الحساسة للسلامة
  • PAT – أداة مجانية للتحقق من النماذج، والمحاكاة، والتحقق من التحسينات للأنظمة المتزامنة وامتدادات CSP (مثل المتغيرات المشتركة، والمصفوفات، والإنصاف)
  • يلف
  • أوبال

حلول ومسابقات

تُعدّ العديد من المسائل في الأساليب الرسمية من المسائل الصعبة من فئة NP ، ولكن يمكن حلّها في الحالات التي تظهر في التطبيق العملي. على سبيل المثال، تُعتبر مسألة إرضاء العبارات المنطقية مسألة كاملة من فئة NP وفقًا لنظرية كوك-ليفين ، ولكن يمكن لبرامج حلّ مسائل SAT حلّ مجموعة متنوعة من الحالات الكبيرة. توجد برامج حلّ لمجموعة متنوعة من المسائل التي تظهر في الأساليب الرسمية، وهناك العديد من المسابقات الدورية لتقييم أحدث التقنيات في حلّ هذه المسائل. [ 35 ]

المنظمات

انظر أيضاً

References

  1. ↑Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ↑Holloway, C. Michael. "Why Engineers Should Consider Formal Methods"(PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from the original(PDF) on 16 November 2006. Retrieved 2006-11-16.{{cite journal}}: Cite journal requires |journal= (help)
  3. ↑Monin, pp.3-4
  4. ↑Utting, Mark; Reeves, Steve (August 31, 2001). "Teaching formal methods lite via testing". Software Testing, Verification and Reliability. 11 (3): 181–195. doi:10.1002/stvr.223.
  5. ↑Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
  6. ↑Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
  7. ↑O'Hearn, Peter W.; Tennent, Robert D. (1997). Algol-like Languages.
  8. ↑Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh (2017). "Program Synthesis". Foundations and Trends in Programming Languages. 4 (1–2): 1–119. doi:10.1561/2500000010.
  9. ↑Gleirscher, Mario; Marmsoler, Diego (November 2020). "Formal methods in dependable systems engineering: a survey of professionals from Europe and North America". Empirical Software Engineering. 25 (6): 4473–4546. arXiv:1812.08815. doi:10.1007/s10664-020-09836-5. ISSN 1573-7616. Retrieved 2026-05-16.
  10. ↑A. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract InterpretationArchived 2015-09-23 at the Wayback Machine. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011).
  11. ↑ بيورنر، داينز؛ هينسون، مارتن سي. (2008). منطق لغات المواصفات . الصفحات من السابع إلى الحادي عشر. 
  12. ↑ براينت، راندال إي. (2018). "مخططات القرار الثنائي". في كلارك، إدموند م.؛ هينزينجر، توماس أ.؛ فيث، هيلموت؛ بلوم، رودريك (محررون). دليل التحقق من النماذج . ص 191. 
  13. ↑ تشاكي، ساجار؛ غورفينكل، آري (2018). "التحقق الرمزي من النماذج القائم على BDD". في كلارك، إدموند م.؛ هينزينجر، توماس أ.؛ فيث، هيلموت؛ بلوم، رودريك (محررون). دليل التحقق من النماذج . ص 191. 
  14. ↑ براساد، موكول ر؛ بير، أرمين؛ غوبتا، آرتي (25 يناير 2005). "دراسة استقصائية للتطورات الحديثة في التحقق الرسمي القائم على SAT". المجلة الدولية لأدوات البرمجيات لنقل التكنولوجيا . 7 (2): 156-173 . doi : 10.1007/s10009-004-0183-4 .
  15. ^ بيورنر، دينس؛ غرام، كريستيان؛ أويست، أولي ن؛ ريستروم، ليف (2011). "مركز دانسك داتاماتيك". في إمباليازو، جون؛ لوندين، لكل؛ وانجلر، بنكت (محرران). تاريخ الحوسبة الشمالية 3: تقدم IFIP في تكنولوجيا المعلومات والاتصالات . سبرينغر. ص 350 – 359. 
  16. ↑ بيورنر، داينز؛ هافيلوند، كلاوس. "أربعون عامًا من الأساليب الرسمية: بعض العقبات وبعض الإمكانيات؟". FM 2014: الأساليب الرسمية: الندوة الدولية التاسعة عشرة، سنغافورة، 12-16 مايو 2014. وقائع المؤتمر (PDF) . سبرينغر. الصفحات 42-61 . 
  17. ↑ جورج، أ. ف.، وأنسيل، إ. (نوفمبر 2008). دمج أنظمة الطائرات بدون طيار في نظام المجال الجوي الوطني. في: أنظمة وخدمات البنية التحتية: بناء شبكات لمستقبل أكثر إشراقًا (INFRA)، المؤتمر الدولي الأول لعام 2008 (ص 1-5). معهد مهندسي الكهرباء والإلكترونيات.
  18. ↑ حل النزاعات والكشف عنها منسقًا جوًا، http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ مؤرشف بتاريخ 5 مارس 2016 في أرشيف الإنترنت
  19. ↑ "أتيليه ب" . www.atelierb.eu .
  20. ↑ CT Chou, PK Mannava, S. Park, " طريقة بسيطة للتحقق من صحة بروتوكولات تماسك ذاكرة التخزين المؤقت "، الأساليب الرسمية في التصميم بمساعدة الحاسوب، ص 382-398، 2004.
  21. ↑ التحقق الرسمي في التحقق من صحة محرك تنفيذ معالج Intel Core i7، http://cps-vo.org/node/1371 مؤرشف في 2015-05-03 في Wayback Machine ، تم الوصول إليه في 13 سبتمبر 2013.
  22. ↑ J. Grundy, "التحسينات التي تم التحقق منها لبنية Intel IA-64"، في إثبات النظرية في منطق الرتبة العليا، Springer Berlin Heidelberg، 2004، ص 215-232.
  23. ↑ E. Seligman, I. Yarom, " أفضل الطرق المعروفة لاستخدام Cadence Conformal LEC "، في Intel.
  24. ↑ سي. إيسنر، أ. ناهير، ك. يوراف، " التحقق الوظيفي من تصميمات البوابات الكهربائية باستخدام الاستدلال التركيبي "", التحقق بمساعدة الحاسوب، سبرينغر برلين هايدلبرغ، ص 433-445.
  25. ↑ PC Attie, H. Chockler, " التحقق التلقائي من محاكاة السجلات المقاومة للأخطاء "، الملاحظات الإلكترونية في علوم الحاسوب النظرية، المجلد 149، العدد 1، الصفحات 49-60.
  26. ↑ KD Schubert, W. Roesner, JM Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, " التحقق الوظيفي من أنظمة المعالج الدقيق IBM POWER7 وأنظمة المعالجات المتعددة POWER7 "، مجلة IBM للبحث والتطوير، المجلد 55، العدد 3.
  27. ↑ X2R-2، التسليم D5.1 .
  28. ↑ دانيال جاكسون وجانيت وينج ، "أساليب رسمية خفيفة الوزن" ، مجلة IEEE Computer ، أبريل 1996
  29. ↑ فينو جورج ورايفورد فون، "تطبيق الأساليب الرسمية الخفيفة في هندسة المتطلبات"، مؤرشف في 1 مارس 2006 على موقع Wayback Machine ، مجلة Crosstalk: The Journal of Defense Software Engineering ، يناير 2003
  30. ↑ دانيال جاكسون، "Alloy: A Lightweight Object Modelling Notation" ، معاملات ACM في هندسة البرمجيات والمنهجية (TOSEM) ، المجلد 11، العدد 2 (أبريل 2002)، الصفحات 256-290
  31. ↑ ريتشارد ديني، النجاح باستخدام حالات الاستخدام: العمل بذكاء لتقديم الجودة ، دار نشر أديسون-ويسلي بروفيشنال، 2005، رقم ISBN 0-321-31643-6.
  32. ↑ ستين أجرهولم وبيتر جي. لارسن، "نهج مبسط للأساليب الرسمية" مؤرشف في 9 مارس 2006 على موقع Wayback Machine ، ضمن وقائع ورشة العمل الدولية حول الاتجاهات الحالية في الأساليب الرسمية التطبيقية ، بوبارد، ألمانيا، سبرينغر-فيرلاغ، أكتوبر 1998
  33. ↑ "ESBMC" . esbmc.org .
  34. ↑ "FizzBee" . fizzbee.io .
  35. ↑ بارتوتشي، إيزيو؛ باير، ديرك؛ بلاك، بول إي.؛ فيديوكوفيتش، غريغوري؛ غارافيل، هوبرت؛ هارتمانز، أرند؛ هويسمان، ماريكي؛ كوردون، فابريس؛ ناجيل، جوليان؛ سيغيريانو، ميهايلا؛ ستيفن، برنارد؛ سودا، مارتن؛ سوتكليف، جيف؛ ويبر، تجارك؛ يامادا، أكيهيسا (2019). "أولمبياد الأدوات 2019: نظرة عامة على المسابقات في الأساليب الرسمية". في: باير، ديرك؛ هويسمان، ماريكي؛ كوردون، فابريس؛ ستيفن، برنارد (محررون). الأدوات والخوارزميات لبناء وتحليل الأنظمة . سلسلة محاضرات في علوم الحاسوب. تشام: دار نشر سبرينغر الدولية. ص 3 – 24. دوى : 10.1007/978-3-030-17502-3_1 . رقم ISBN  978-3-030-17502-3.
  36. ^ فروليكس، نيلز. هيول، مارين؛ إيزر، ماركوس؛ يارفيسالو، ماتي؛ سودا ، مارتن (2021-12-01). "مسابقة السات 2020" . الذكاء الاصطناعي . 301 103572. دوى : 10.1016/j.artint.2021.103572 . اتش دي ال : 10138/335114 . ISSN 0004-3702 . 
  37. ↑ كورنيخو، سيزار (27 يناير 2021). "دعم حسابي قائم على SAT لـ Alloy" . وقائع المؤتمر الدولي الخامس والثلاثين لهندسة البرمجيات الآلية IEEE/ACM . ASE '20. نيويورك، نيويورك، الولايات المتحدة الأمريكية: رابطة آلات الحوسبة. الصفحات 1161-1163 . doi : 10.1145/3324884.3415285 . ISBN  978-1-4503-6768-4.
  38. ↑ باريت، كلارك؛ ديترز، مورغان؛ دي مورا، ليوناردو؛ أوليفيراس، ألبرت؛ ستامب، آرون (2013-03-01). "ست سنوات من SMT-COMP" . مجلة الاستدلال الآلي . 50 (3): 243-277 . doi : 10.1007/s10817-012-9246-5 . ISSN 1573-0670 . 
  39. ↑ فيديوكوفيتش، غريغوري؛ رومر، فيليب (13 سبتمبر 2021). "تقرير المسابقة: CHC-COMP-21" . وقائع إلكترونية في علوم الحاسوب النظرية . 344 : 91-108 . arXiv : 2008.02939 . doi : 10.4204/EPTCS.344.7 . ISSN 2075-2180 . 
  40. ↑ شوكلا، أنكيت؛ بير، أرمين؛ بولينا، لوكا؛ سيدل، مارتينا (نوفمبر 2019). "دراسة استقصائية حول تطبيقات الصيغ المنطقية الكمية". المؤتمر الدولي الحادي والثلاثون لأدوات الذكاء الاصطناعي (ICTAI) لعام 2019. معهد مهندسي الكهرباء والإلكترونيات. الصفحات 78-84 . doi : 10.1109/ICTAI.2019.00020 . ISBN  978-1-7281-3798-8.
  41. ^ بولينا، لوكا؛ سيدل ، مارتينا (2019/09/01). "تقييمات حلول QBF لعامي 2016 و2017 (QBFEVAL'16 وQBFEVAL'17)" . الذكاء الاصطناعي . 274 : 224– 248. دوى : 10.1016/j.artint.2019.04.002 . ISSN 0004-3702 . 
  42. ↑ باير، ديرك (2022). "التقدم في التحقق من البرمجيات: SV-COMP 2022". في: فيسمان، دانا؛ روسو، غريغوري (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة . سلسلة محاضرات في علوم الحاسوب. المجلد 13244. تشام: دار نشر سبرينغر الدولية. الصفحات 375-402 . doi : 10.1007/978-3-030-99527-0_20 . ISBN   978-3-030-99527-0.
  43. ↑ ألور، راجيف؛ فيسمان، دانا؛ سينغ، ريشاب؛ سولار-ليزاما، أرماندو (28-11-2017). "SyGuS-Comp 2017: النتائج والتحليل" . وقائع إلكترونية في علوم الحاسوب النظرية . 260 : 97-115 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . 

للمزيد من القراءة

مواد أرشيفية