Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

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

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

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

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

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

كانت نتائج تجاربهم مذهلة. ففي الحالات التي تمت فيها برمجة الروبوتات بسرعات آمنة وأوقات انتظار متنوعة، أكد مدقق النموذج أن جميع الروبوتات الخمسة ستصل إلى وجهاتها دون الاصطدام ببعضها البعض أو التعثر. ثم قام الباحثون بتشغيل كود ROS2 الفعلي في محاكاة، وتصرفت الروبوتات تماماً كما توقع النموذج، حيث تنقلت في المساحة المزدحمة بنجاح. ومع ذلك، عندما غيروا المعايير لخلق موقف خطير — مثل جعل جميع الروبوتات تتحرك بنفس السرعة تماماً أو ضبط معدل المسح ليكون منخفضاً جداً بالنسبة للسرعة — وجد مدقق النموذج خللاً على الفور. لقد حدد تسلسلاً معيناً من الأحداث يؤدي إلى تصادم. وعندما قاموا بتشغيل الكود الحقيقي مع هذه الإعدادات الخطيرة نفسها، تعطلت المحاكاة بنفس الطريقة التي توقعها النموذج. وفي أحد الاختبارات، وجد النموذج تصادماً بعد استكشاف بضعة آلاف من الحالات فقط، بينما فشلت المحاكاة الحقيقية في ثلاث من أصل خمس مرات، مما أكد أن الخطر كان حقيقياً ويمكن التنبؤ به.

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

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

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