طريقة ب
طريقة B هي طريقة لتطوير البرمجيات تعتمد على B ، وهي طريقة رسمية مدعومة بالأدوات تعتمد على تدوين آلة مجردة ، وتستخدم في تطوير برامج الحاسوب . [ 1 ] [ 2 ]
بالمقارنة مع تدوين Z ، فإن لغة B أكثر دقةً وتركيزًا على تحسين الكود بدلًا من مجرد المواصفات الرسمية ، ولذلك يسهل تنفيذ المواصفات المكتوبة بلغة B بشكل صحيح مقارنةً بتلك المكتوبة بلغة Z. وتتوفر أدوات دعم جيدة لهذا الغرض. وتُستخدم اللغة نفسها في المواصفات والتصميم والبرمجة، وتشمل آلياتها التغليف وموقع البيانات.
تاريخ
طُوِّرت لغة البرمجة B في الأصل في ثمانينيات القرن الماضي على يد جان ريمون أبريال [ 3 ] [ 4 ] في فرنسا والمملكة المتحدة . [ 5 ] ترتبط B بترميز Z (الذي ابتكره أبريال أيضًا) وتدعم تطوير أكواد لغات البرمجة انطلاقًا من المواصفات. استُخدمت B في تطبيقات أنظمة بالغة الأهمية للسلامة في أوروبا (مثل خطي مترو باريس الآليين 14 و 1 وصاروخ أريان 5 ). [ 6 ] [ 7 ] [ 8 ] تتميز B بدعم قوي ومتوفر تجاريًا لأدوات تحديد المواصفات والتصميم والتحقق من صحة الكود وتوليده .
منذ أواخر ثمانينيات القرن العشرين، كان إيب هولم سورنسن (1949-2012) شخصية محورية في تطوير طريقة B، [ 9 ] [ 10 ] بعد أن عمل سابقًا على التطوير المبكر لترميز Z. ترك مختبر الحوسبة بجامعة أكسفورد ليقود فريقًا في شركة BP Research [ 11 ] وليطور مجموعة أدوات B، التي توفر الدعم البرمجي لطريقة B. لاحقًا، أسس شركة B-Core (UK) Limited لدعم مجموعة أدوات B، [ 12 ] [ 13 ] وهي عبارة عن مجموعة من أدوات البرمجة المصممة لدعم استخدام ترميز B، وساهم في إنجاز عدد من المشاريع المتعلقة بـ B.
الحدث-ب
لاحقًا، طُوِّرت طريقة رسمية أخرى تُسمى Event-B [ 14 ] [ 15 ] [ 16 ] استنادًا إلى طريقة B، بدعم من منصة Rodin . [ 17 ] [ 18 ] تُعدّ Event-B طريقة رسمية تهدف إلى نمذجة وتحليل الأنظمة على مستوى النظام. ومن سمات Event-B استخدام نظرية المجموعات للنمذجة، واستخدام التحسين لتمثيل الأنظمة على مستويات تجريد مختلفة، واستخدام البرهان الرياضي للتحقق من الاتساق بين مستويات التحسين هذه.
المكونات الرئيسية
تعتمد صيغة B على نظرية المجموعات ومنطق الرتبة الأولى لتحديد مستويات مختلفة من وصف البرمجيات التي تغطي الدورة الكاملة لتطوير المشروع.
آلة تجريدية
في النسخة الأولى والأكثر تجريدًا، والتي تسمى الآلة المجردة ، يجب على المصمم تحديد هدف التصميم.
التحسين
- ثم، خلال خطوة التحسين، قد يقومون بتوسيع المواصفات من أجل توضيح الهدف أو لجعل الآلة المجردة أكثر واقعية من خلال إضافة تفاصيل حول هياكل البيانات والخوارزميات التي تحدد كيفية تحقيق الهدف.
- يجب إثبات أن النسخة الجديدة، والتي تسمى "التحسين "، متماسكة وتتضمن جميع خصائص الآلة المجردة.
- قد يستخدم المصمم مكتبات B من أجل نمذجة هياكل البيانات أو لتضمين أو استيراد المكونات الموجودة.
تطبيق
- يستمر التحسين حتى يتم التوصل إلى نسخة حتمية: التنفيذ .
- خلال جميع مراحل التطوير، يتم استخدام نفس الترميز، ويمكن ترجمة الإصدار الأخير إلى لغة برمجة من أجل التجميع.
برمجة
يوجد عدد من البرامج التي تدعم طريقة B و Event-B.
أتيليه ب
يُعدّ Atelier B ، الذي طورته شركة ClearSy، أداةً صناعيةً تُتيح الاستخدام العملي لمنهجية B لتطوير برمجيات مُثبتة وخالية من العيوب (برمجيات رسمية). يتوفر إصداران: 1) الإصدار المجاني، المُتاح للجميع دون أي قيود؛ 2) إصدار الصيانة، المُخصص لحاملي عقود الصيانة فقط. وقد استُخدم Atelier B لتطوير أنظمة أمان آلية لمختلف خطوط مترو الأنفاق التي أنشأتها شركتا Alstom وSiemens حول العالم ، وكذلك للحصول على شهادة المعايير المشتركة وتطوير نماذج الأنظمة من قِبل شركتي ATMEL و STMicroelectronics .
مجموعة أدوات B
مجموعة أدوات B [ 21 ] [ 22 ] هي مجموعة من أدوات البرمجة المصممة لدعم استخدام أداة B، [ 23 ] وهي مترجم رياضي قائم على نظرية المجموعات لدعم طريقة B. وقد تولى تطويرها في الأصل إيب هولم سورنسن وآخرون في شركة BP Research، ثم في شركة B-Core (المملكة المتحدة) المحدودة. [ 10 ]
تستخدم مجموعة الأدوات واجهة X Window Motif مخصصة [ 24 ] لإدارة واجهة المستخدم الرسومية، وتعمل بشكل أساسي على أنظمة التشغيل لينكس ، وماك أو إس إكس ، وسولاريس . يتوفر كود مصدر B-Toolkit على GitHub . [ 25 ]
انقر وأثبت
توفر أداة Click'n'Prove بيئة لإنشاء وإلغاء التزامات الإثبات، وللتحقق من الاتساق والتحسين. [ 26 ]
احتمال
ProB هي أداة برمجية متكاملة للرسوم المتحركة ومدقق النماذج لمنهجية B. [ 27 ] تُمكّن من عرض الرسوم المتحركة للعديد من مواصفات B، كما يمكنها التحقق بشكل منهجي من أنواع مختلفة من الأخطاء في المواصفات. تتضمن ProB أدوات لحل القيود ، والتي يمكن استخدامها للمساعدة في التحقق من حالات الجمود ، واكتشاف النماذج، وتوليد حالات الاختبار . طُوّرت هذه الأداة من قِبل مجموعة STUPS في جامعة هاينريش هاينه في دوسلدورف . [ 28 ]
رودان
منصة رودين هي أداة تدعم Event-B . [ 14 ] [ 29 ] [ 17 ] تعتمد رودين على بيئة تطوير متكاملة (IDE) من إكليبس ، وتوفر دعمًا للتحسين والبرهان الرياضي . المنصة مفتوحة المصدر وتشكل جزءًا من إطار عمل إكليبس، ويمكن توسيعها باستخدام إضافات برمجية . وقد حظي تطوير رودين بدعم من مشاريع الاتحاد الأوروبي : DEPLOY (2008-2012)، وRODIN (2004-2007)، وADVANCE (2011-2014). [ 14 ]
آحرون
توفر لغة BHDL طريقة للتصميم الصحيح للدوائر الرقمية ، حيث تجمع بين مزايا لغة وصف الأجهزة VHDL وشكلية B. [ 30 ]
APCB
نظمت APCB ( بالفرنسية : Association de Pilotage des Conférences B ، أي اللجنة التوجيهية الدولية لمؤتمر B ) اجتماعات مرتبطة بمنهجية B. [ 31 ] كما نظمت مؤتمرات ZB مع مجموعة مستخدمي Z ومؤتمرات ABZ، بما في ذلك آلات الحالة المجردة (ASM) بالإضافة إلى تدوين Z.
الكتب
- كتاب "ب: إسناد البرامج إلى المعاني" ، جان ريمون أبريال ، مطبعة جامعة كامبريدج ، 1996. رقم ISBN 0-521-49619-5.
- طريقة B: مقدمة ، ستيف شنايدر، بالغراف ماكميلان ، سلسلة ركائز الحوسبة، 2001. ISBN 0-333-79284-X.
- هندسة البرمجيات باستخدام لغة B ، جون وردزورث، أديسون ويسلي لونغمان ، 1996. ISBN 0-201-40356-0.
- لغة ومنهج B: دليل للتطوير الرسمي العملي ، كيفن لانو ، سبرينغر-فيرلاغ ، سلسلة FACIT، 1996. ISBN 3-540-76033-4.
- المواصفات في لغة B: مقدمة باستخدام مجموعة أدوات B ، كيفن لانو ، شركة النشر العالمية العلمية ، مطبعة إمبريال كوليدج ، 1996. ISBN 1-86094-008-0.
- النمذجة في Event-B: هندسة النظم والبرمجيات ، جان ريمون أبريال ، مطبعة جامعة كامبريدج ، 2010. ISBN 978-0-521-89556-9.
المؤتمرات
وقد تضمنت المؤتمرات التالية بشكل صريح طريقة B و/أو الحدث B: [ 32 ]
- مؤتمر Z2B، نانت ، فرنسا ، 10-12 أكتوبر 1995
- المؤتمر الأول B، نانت، فرنسا، 25-27 نوفمبر 1996
- المؤتمر الثاني B، مونبلييه ، فرنسا، 22-24 أبريل 1998
- ZB 2000، يورك ، المملكة المتحدة ، 28 أغسطس - 2 سبتمبر 2000
- ZB 2002، غرونوبل ، فرنسا، 23-25 يناير 2002
- ZB 2003، توركو ، فنلندا ، 4-6 يونيو 2003
- ZB 2005، غيلدفورد ، المملكة المتحدة، 2005
- ب 2007، بيزانسون ، فرنسا، 2007
- ب، من البحث إلى التدريس، نانت، فرنسا، 16 يونيو 2008
- ب، من البحث إلى التدريس، نانت، فرنسا، 8 يونيو 2009
- ب، من البحث إلى التدريس، نانت، فرنسا، 7 يونيو 2010
- ABZ 2008، BCS ، لندن ، المملكة المتحدة، 16-18 سبتمبر 2008
- ABZ 2010، أورفورد ، كيبيك ، كندا ، 23-25 فبراير 2010
- ABZ 2012، بيزا ، إيطاليا ، 18-22 يونيو 2012
- ABZ 2014، تولوز ، فرنسا، 2-6 يونيو 2014
- ABZ 2016، لينز ، النمسا ، 23-27 مايو 2016
- مؤتمر ABZ 2018، ساوثهامبتون ، المملكة المتحدة، 5-8 يونيو 2018
- ABZ 2020، أولم ، ألمانيا ، 9-13 يونيو 2020 (تأجل بسبب جائحة كوفيد-19 )
- مؤتمر ABZ 2021، أولم، ألمانيا، 9-13 يونيو 2021
- ABZ 2023، نانسي ، فرنسا، 30 مايو - 2 يونيو 2023
- ABZ 2024، بيرغامو ، إيطاليا ، 25-28 2024
- ABZ 2025، دوسلدورف ، ألمانيا، 10-13 يونيو 2025
- ABZ 2026، طوكيو ، اليابان، 18-20 مايو 2026
انظر أيضاً
مراجع
- ↑ كانسيل، دومينيك، ودومينيك ميري. "أسس طريقة B". الحوسبة والمعلوماتية 22، العدد 3-4 (2003): 221-256.
- ↑ باتلر، مايكل، وفيليب كورنر، وسيباستيان كرينغز، وتيري لوكونت، ومايكل لويشل، ولويس فرناندو ميخيا، ولوران فوازان. "الخمسة والعشرون عامًا الأولى من الاستخدام الصناعي لمنهجية B". في المؤتمر الدولي حول الأساليب الرسمية للأنظمة الصناعية الحرجة، الصفحات 189-209. سبرينغر ، تشام، 2020.
- ↑ جان ريموند أبريال (1988). "أداة B (ملخص)" (ملف PDF) . في: بلومفيلد، روبن إي؛ مارشال، لين إس؛ جونز، روجر بي (محررون). VDM – الطريق إلى الأمام، وقائع ندوة VDM-Europe الثانية . سلسلة محاضرات في علوم الحاسوب . المجلد 328. سبرينغر. الصفحات 86-87 . doi : 10.1007/3-540-50214-9_8 . ISBN 978-3-540-50214-2.
- ↑ أبريال، جيه آر، ماثيو كي أو لي، دي إس نيلسون، بي إن شارباخ، وإيب هولم سورنسن. "طريقة بي". في الندوة الدولية لـ VDM Europe، الصفحات 398-405. سبرينغر، برلين، هايدلبرغ، 1991.
- ↑ بوين، جوناثان ب .؛ هابرياس، هنري (أبريل–يونيو 2025). "جان ريموند أبريال: سيرة علمية لرائد في الأساليب الرسمية". حوليات معهد مهندسي الكهرباء والإلكترونيات لتاريخ الحوسبة . 48 (2). جمعية الحاسبات التابعة لمعهد مهندسي الكهرباء والإلكترونيات : 71–80 . arXiv : 2604.07353 . doi : 10.1109/MAHC.2026.3685515 .
- ↑ جيرهارت، سوزان، د. كريجن، وتيد رالستون. "دراسة حالة: نظام إشارات مترو باريس." IEEE Software 11، العدد 1 (1994): 32-28.
- ↑ بيهم، باتريك، بول بينوا، آلان فايفر، وجان مارك مينادير. "ميتيور: تطبيق ناجح لـ B في مشروع كبير." في الندوة الدولية حول الأساليب الرسمية، الصفحات 369-387. سبرينغر، برلين، هايدلبرغ، 1999.
- ↑ لوكونت، تييري. "تطبيق المنهج الرسمي في الصناعة: مسار 15 عامًا". في ورشة العمل الدولية حول الأساليب الرسمية للأنظمة الصناعية الحرجة، ص 26-34. سبرينغر، برلين، هايدلبرغ، 2009.
- ↑ بهاتاشاريا، سوراف؛ وينتر، فيكتور ل.، محرران. (2012). "8. تاريخ لغة B". برمجيات عالية الموثوقية. سبرينغر . ص 40. ISBN 978-1461513919.
- 1 2 بوين، جوناثان (يوليو 2022). "إيب هولم سورنسن: بعد عشر سنوات" (ملف PDF) . حقائق FACS ( 2022-2 ). BCS-FACS : 41-49 . تم الاطلاع عليه في 3 أغسطس 2022 .
- ↑ كريشتون، إدوارد (29 مارس 2022). " BToolkit ". GitHub.
- ↑ روسكو، بيل (8 فبراير 2012). " إيب سورنسن - في ذكرى وفاته ". قسم علوم الحاسوب، جامعة أكسفورد ، المملكة المتحدة.
- ↑ ووردزورث، ج. ب. (1996). هندسة البرمجيات مع ب. أديسون-ويسلي. رقم ISBN 978-0201403565
- 1 2 3 "Event-B ومنصة رودان" . Event-B.org .
- ↑ بتلر، مايكل. "هياكل التفكيك للحدث-ب." في المؤتمر الدولي حول الأساليب الرسمية المتكاملة، ص 20-38. سبرينغر، برلين، هايدلبرغ، 2009.
- ↑ أبريال، جان ريموند. النمذجة في Event-B: هندسة النظم والبرمجيات. مطبعة جامعة كامبريدج ، 2010.
- 1 2 أبريال، جان ريموند، مايكل بتلر، ستيفان هالرستيد، تاي سون هوانغ، فرهاد ميهتا، ولوران فوازان. "رودين: مجموعة أدوات مفتوحة المصدر للنمذجة والاستدلال في Event-B." المجلة الدولية لأدوات البرمجيات لنقل التكنولوجيا 12، العدد 6 (2010): 447-466.
- ↑ هوانغ، تاي سون، أندرياس فورست، وجان ريموند أبريال. "أنماط Event-B ودعم أدواتها." نمذجة البرمجيات والأنظمة 12، العدد 2 (2013): 229-244.
- ↑ "AtelierB.eu" .
- ↑ مينتري، ديفيد، كلود مارشيه، جان كريستوف فيلياتر، وماساشي أسوكا. "التخلص من التزامات الإثبات من أتيليه ب باستخدام أدوات إثبات آلية متعددة." في المؤتمر الدولي حول آلات الحالة المجردة، ألوي، ب، في دي إم، وزد، الصفحات 238-251. سبرينغر، برلين، هايدلبرغ، 2012.
- ↑ "مجموعة أدوات B" . [شركة B-Core (المملكة المتحدة) المحدودة] . 2004. مؤرشف من الأصل في 12 أكتوبر 2004. تم الاطلاع عليه في 22 فبراير 2012 .
- ↑ هوتون، هوارد، وكيفن لانو. المواصفات في لغة B: مقدمة باستخدام مجموعة أدوات B. وورلد ساينتيفيك، 1996.
- ↑ أبريال، جان ريموند. "أداة B". في الندوة الدولية لـ VDM Europe، الصفحات 86-87. سبرينغر، برلين، هايدلبرغ، 1988.
- ↑ متطلبات مجموعة أدوات B مؤرشفة بتاريخ 12-10-2004 على موقع Wayback Machine
- ↑ كريشتون، إدوارد. "شفرة مصدر B-Toolkit" . جيت هاب .
- ↑ أبريال، جيه.-آر.؛ كانسيل، دي. (2003). "انقر وأثبت: براهين تفاعلية ضمن نظرية المجموعات". في: باسين، دي.؛ وولف، بي. (محرران). إثبات النظريات في منطق الرتبة العليا (TPHOLs) . سلسلة محاضرات في علوم الحاسوب . المجلد 2758. برلين، هايدلبرغ: سبرينغر. doi : 10.1007/10930755_1 .
- ↑ "ما هو ProB؟" . ألمانيا: جامعة هاينريش هاينه دوسلدورف . تم الاطلاع عليه بتاريخ 28 مارس 2026 .
- ↑ "ProB؟" . railML.org . تم الاطلاع عليه بتاريخ 28 مارس 2026 .
- ↑ أبريال، جيه آر. "عملية تطوير نظام باستخدام Event-B ومنصة Rodin." في المؤتمر الدولي حول أساليب الهندسة الرسمية، الصفحات 1-3. سبرينغر، برلين، هايدلبرغ، 2007.
- ↑ ألجير، عمار، فيليب ديفيين، صوفي تيسون ، جيه إل. بولانجر، وجورج ماريانو. "BHDL: تصميم الدوائر في B." في وقائع المؤتمر الدولي الثالث حول تطبيق التزامن على تصميم الأنظمة، الصفحات 241-242. IEEE، 2003.
- ^ "رابطة إرشاد المؤتمرات ب" . librairiecosmopolite.com . تم الاسترجاع في 27 يوليو 2022 .
- ↑ "المؤتمرات" . ABZ . تم الاطلاع عليه بتاريخ 16 يناير 2026 .
روابط خارجية
- موقع أتيليه بي الإلكتروني
- الموقع ب غرونوبل
- الأساليب الرسمية
- أدوات الأساليب الرسمية
- لغات المواصفات الرسمية