طريقة شكلية

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

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

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

التصنيف

[عدل]

يمكن استخدام الطرق الشكلية على مجموعة من المستويات:

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

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

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

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

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

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

الطرق الشكلية الخفيفة

[عدل]

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

انظر أيضًا

[عدل]

المراجع

[عدل]
  1. ^ R. W. Butler (6 أغسطس 2001). "What is Formal Methods?". مؤرشف من الأصل في 2017-02-13. اطلع عليه بتاريخ 2006-11-16.
  2. ^ C. Michael Holloway. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). مؤرشف من الأصل (PDF) في 2012-06-06. اطلع عليه بتاريخ 2006-11-16. {{استشهاد بدورية محكمة}}: الاستشهاد بدورية محكمة يطلب |دورية محكمة= (مساعدة)
  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 على موقع واي باك مشين.

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

كتابات أخرى

[عدل]

وصلات خارجية

[عدل]
في كومنز صور وملفات عن Formal methods.