مكاملة لغة توصيف العتاد BHDL ضمن بيئة Eclipse

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