المواصفات الرسمية

الموسوعة الحرة

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

تحفيز

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

الاستخدامات

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

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

يجب أن تتضمن المواصفات الجيدة بعض السمات التالية: كافية، متسقة داخلياً، غير غامضة، كاملة، مُرضية، دنيا. [ 3 ]

المواصفات الجيدة ستتضمن ما يلي: [ 3 ]

  • قابلية الإنشاء، وقابلية الإدارة، وقابلية التطوير
  • سهولة الاستخدام
  • قابلية التواصل
  • تحليل قوي وفعال

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

القيود

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

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

  • وقت
    • تكلفة بدء تشغيل أولية مرتفعة مع عوائد قابلة للقياس منخفضة
  • المرونة
    • تستخدم العديد من شركات البرمجيات منهجيات رشيقة تركز على المرونة. وغالبًا ما يُنظر إلى وضع مواصفات رسمية للنظام بأكمله مسبقًا على أنه نقيض المرونة. ومع ذلك، توجد بعض الأبحاث التي تتناول فوائد استخدام المواصفات الرسمية مع التطوير الرشيق [ 5 ].
  • تعقيد
    • إنها تتطلب مستوى عالٍ من الخبرة الرياضية والمهارات التحليلية لفهمها وتطبيقها بفعالية [ 5 ]
    • يتمثل أحد الحلول في تطوير أدوات ونماذج تسمح بتنفيذ هذه التقنيات ولكنها تخفي الرياضيات الأساسية [ 2 ] [ 5 ]
  • نطاق محدود [ 3 ]
    • إنها لا تلتقط الخصائص التي تهم جميع أصحاب المصلحة في المشروع [ 3 ]
    • إنهم لا يقومون بعمل جيد في تحديد واجهات المستخدم وتفاعل المستخدم [ 4 ]
  • غير مجدٍ اقتصادياً
    • هذا ليس صحيحًا تمامًا؛ فقد أثبتت فعاليتها من حيث التكلفة من خلال حصر استخدامها في الأجزاء الأساسية فقط من الأنظمة الحيوية [ 4 ].

قيود أخرى: [ 3 ]

  • عزل
  • الأنطولوجيات منخفضة المستوى
  • توجيه ضعيف
  • ضعف فصل الاهتمامات
  • ضعف استجابة الأداة

النماذج

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

  • المواصفات القائمة على التاريخ [ 3 ]
    • السلوك بناءً على تاريخ النظام
    • يتم تفسير الادعاءات بمرور الوقت
  • المواصفات القائمة على الحالة [ 3 ]
    • السلوك بناءً على حالات النظام
    • سلسلة من الخطوات المتسلسلة، (على سبيل المثال، معاملة مالية)
    • تعتمد لغات مثل Z أو VDM أو B على هذا النموذج [ 3 ]
  • المواصفات القائمة على الانتقال [ 3 ]
    • سلوك قائم على الانتقالات من حالة إلى أخرى للنظام
    • يُفضل استخدامه مع نظام تفاعلي
    • تعتمد لغات مثل Statecharts و PROMELA و STeP-SPL و RSML أو SCR على هذا النموذج [ 3 ].
  • المواصفات الوظيفية [ 3 ]
    • حدد النظام كهيكل من الدوال الرياضية
    • تعتمد OBJ و ASL و PLUSS و LARCH و HOL أو PVS على هذا النموذج [ 3 ]
  • المواصفات التشغيلية [ 3 ]
    • تعتمد اللغات المبكرة مثل Paisley و GIST و Petri nets أو جبر العمليات على هذا النموذج [ 3 ].
  • لغات متعددة النماذج
    • FizzBee هي لغة مواصفات متعددة النماذج تسمح بالمواصفات القائمة على الانتقال/الإجراء، والمواصفات السلوكية مع انتقالات غير ذرية، ولديها أيضًا نموذج الممثل.

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

أدوات البرمجيات

تُعدّ لغة Z مثالاً على لغة مواصفات رسمية رائدة . ومن اللغات الأخرى لغة المواصفات (VDM-SL) الخاصة بمنهجية فيينا للتطوير ، ولغة الآلة المجردة (AMN) الخاصة بمنهجية B. في مجال خدمات الويب ، تُستخدم المواصفات الرسمية غالبًا لوصف الخصائص غير الوظيفية [ 7 ] ( جودة خدمة خدمات الويب ).

بعض الأدوات هي: [ 4 ]

مراجع

  1. 1 2 هيرونز، آر إم؛ بوغدانوف، ك؛ بوين، جيه بي ؛ كليفلاند، آر؛ ديريك، جيه؛ ديك، جيه؛ غيورغي، إم؛ هارمان، إم ؛ كابور، ك؛ كراوس، بي؛ لوتجن، جي؛ سيمونز، إيه جيه إتش؛ فيلكومير، إس إيه ؛ وودوارد، إم آر؛ زيدان، إتش. (2009). "استخدام المواصفات الرسمية لدعم الاختبار". مجلة ACM Computing Surveys . 41 (2): 1. CiteSeerX 10.1.1.144.3320 . doi : 10.1145/1459352.1459354 . S2CID 10686134 .  
  2. 1 2 3 4 5 غوديل، م.-س. (1994). "تقنيات المواصفات الرسمية". وقائع المؤتمر الدولي السادس عشر لهندسة البرمجيات . ص 223-227 . doi : 10.1109/ICSE.1994.296781 . ISBN  978-0-8186-5855-6. S2CID 60740848 . 
  3. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 لامسويرد، أ. ف. ( 2000). "المواصفات الرسمية". وقائع مؤتمر مستقبل هندسة البرمجيات - ICSE '00 . الصفحات 147-159 . doi : 10.1145/336512.336546 . ISBN  978-1581132533. S2CID 4657483 . 
  4. 1 2 3 4 سومرفيل، إيان (2009). "المواصفات الرسمية" (ملف PDF) . هندسة البرمجيات . تم الاطلاع عليه في 3 فبراير 2013 .
  5. 1 2 3 نومينما، تيمو؛ تينسو، أليكسي؛ بيركي، إيليني؛ ميكونين، تومي؛ كويتينن، جوسي؛ كولتيما ، أناكايسا (4 أغسطس 2011). “دعم التطوير السريع من خلال تسهيل تفاعل المستخدم الطبيعي مع المواصفات الرسمية القابلة للتنفيذ”. ACM SIGSOFT ملاحظات هندسة البرمجيات . 36 (4): 1– 10. دوى : 10.1145/1988997.2003643 . S2CID 2139235 . 
  6. 1 2 فان دير بول، جون أ.؛ باولا كوتزي (2002). "ما هي أساليب التصميم التي قد تعزز فائدة المواصفات الرسمية؟" . وقائع المؤتمر البحثي السنوي لعام 2002 للمعهد الجنوب أفريقي لعلماء الحاسوب وتقنيي المعلومات حول التمكين من خلال التكنولوجيا . SAICSIT '02: 179-194 . ISBN 9781581135961.
  7. ↑ نموذج المعرفة S-Cube: المواصفات الرسمية