أساليب رسمية

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

مثال على المواصفات الشكلية باستخدام تدوين زد.

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

التصنيف

يمكن استخدام الأساليب الشكلية على مجموعة من المستويات:

المستوى 0: المواصفات الشكلية يمكن تنفيذها وبالتالي يمكن تطوير برنامج منها بشكل غير شكلي. وقد أطلق على ذلك اسم الأساليب الشكلية الخفيفة. ويمكن أن يكون هذا الخيار هو أفضل الخيارات من ناحية التكلفة في العديد من الحالات.

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

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

وهناك المزيد من المعلومات حول هذا الأمر أدناه.

وكما هو الحال في سيمانتيك لغة البرمجة، فإن أنماط الأساليب الشكلية يمكن أن يتم تصنيفها بشكل تقريبي كما يلي:

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

الأساليب الشكلية الخفيفة

يرى بعض الممارسين أن مجتمع الأساليب الشكلية قد ركز بشكل زائد عن الحد على الشكلية الكاملة للمواصفة أو التصميم.[4][5] وهم يؤكدون أن درجة التعبير عن اللغات المضمنة، بالإضافة إلى درجة تعقيد الأنظمة التي يتم وضع نماذج لها، تجعل الشكلية الكاملة مهمة صعبة ومكلفة. وكبديل لذلك، تم اقتراح العديد من الأساليب الشكلية الخفيفة، والتي تركز على المواصفة الجزئية والتطبيق الذي يتم التركيز عليه. وتشتمل أمثلة هذه المنهجية الخفيفة للأساليب الشكلية على ملاحظات نمذجة كائن لغة ألوي،[6] وتوليف ديني لبعض أوجه تدوين زد مع التطوير المشتق من حالة الاستخدام،[7] وأدوات CSK أسلوب تطوير فيينا (VDM).[8]

انظر أيضًا

المراجع
  1. R. W. Butler (2001-08-06). "What is Formal Methods?". مؤرشف من الأصل في 13 فبراير 2017. اطلع عليه بتاريخ 16 نوفمبر 2006. الوسيط |CitationClass= تم تجاهله (مساعدة)
  2. C. Michael Holloway. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). مؤرشف من الأصل (PDF) في 6 يونيو 2012. اطلع عليه بتاريخ 16 نوفمبر 2006. الوسيط |CitationClass= تم تجاهله (مساعدة); Cite journal requires |journal= (مساعدة)
  3. Monin, pp.3-4
  4. دانييل جاكسون and جانيت وينغ, "Lightweight Formal Methods", IEEE Computer, April 1996 نسخة محفوظة 06 ديسمبر 2016 على موقع واي باك مشين.
  5. Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003 نسخة محفوظة 24 سبتمبر 2010 على موقع واي باك مشين.
  6. Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290 نسخة محفوظة 22 سبتمبر 2009 على موقع واي باك مشين.
  7. Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  8. Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998 نسخة محفوظة 22 سبتمبر 2009 على موقع واي باك مشين.

    تستند هذة المقالة على مواد من قاموس الحوسبة المجاني على الانترنت، وهو ترخيص تحت رخصة جنو للوثائق الحرة.

    كتابات أخرى
    • Jean François Monin and Michael G. Hinchey, Understanding formal methods, سبرنجر, 2003, ISBN 1-85233-247-6.
    • جوناثان بوين and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering,Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, رابطة مكائن الحوسبة, 2004.
    • Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.

    وصلات خارجية
    في كومنز صور وملفات عن: أساليب رسمية
    • بوابة علم الحاسوب
    • بوابة تقنية المعلومات
    This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.