أساليب رسمية

من ويكيبيديا، الموسوعة الحرة
اذهب إلى: تصفح، ‏ ابحث
مثال على المواصفات الشكلية باستخدام تدوين زد.

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

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

التصنيف[عدل]

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

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

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

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

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

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

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

الأساليب الشكلية الخفيفة[عدل]

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

انظر أيضًا[عدل]

المراجع[عدل]

  1. ^ R. W. Butler (2001-08-06). "What is Formal Methods?". اطلع عليه بتاريخ 2006-11-16. 
  2. ^ C. Michael Holloway. Why Engineers Should Consider Formal Methods. 16th Digital Avionics Systems Conference (27–30 October 1997). اطلع عليه بتاريخ 2006-11-16. 
  3. ^ Monin, pp.3-4
  4. ^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
  5. ^ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003
  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
  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

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


كتابات أخرى[عدل]

وصلات خارجية[عدل]