توليف برنامج تشغيل الجهاز والتحقق منه

📅 آخر تحديث: ٢٩ يوليو ٢٠٢٦
✍️ نُشر في: ٢٩ يوليو ٢٠٢٦
📷 يحتوي على 1 صور
الموسوعة الحرة
بنية برنامج تشغيل الجهاز.
برنامج تشغيل الجهاز

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

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

الدافع وراء توليف برامج التشغيل والتحقق منها تلقائيًا

تُعدّ برامج تشغيل الأجهزة المكوّن الرئيسي المُعرّض للأعطال في معظم الأنظمة. وقد وجد مشروع بيركلي للبنية التحتية المفتوحة للحوسبة الشبكية (BOINC) أن أعطال أنظمة التشغيل تنتج في الغالب عن رداءة كتابة كود برامج تشغيل الأجهزة. [ 1 ] في نظام التشغيل ويندوز إكس بي ، تُشكّل برامج التشغيل 85% من حالات الفشل المُبلّغ عنها. وفي نواة لينكس 2.4.1، يُمثّل كود برامج تشغيل الأجهزة حوالي 70% من حجم الكود. [ 2 ] قد يؤدي عطل برنامج التشغيل إلى انهيار النظام بأكمله نظرًا لتشغيله في وضع النواة . وقد أسفرت هذه النتائج عن ظهور منهجيات وتقنيات مُتنوّعة للتحقق من برامج تشغيل الأجهزة. وكان من بين البدائل تطوير تقنيات قادرة على توليد برامج تشغيل الأجهزة بكفاءة عالية. إنّ تقليل التدخل البشري في عملية التطوير والتحديد الدقيق للجهاز ونظام التشغيل يُمكن أن يُؤدّي إلى برامج تشغيل أكثر موثوقية.

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

التحقق من برامج تشغيل الأجهزة

هناك تحديان يحدان من اختبار برامج تشغيل الأجهزة.

  • يصعب تحديد العملية أو الوقت الدقيقين لحدوث خلل في التفاعل بين برنامج التشغيل ونواة النظام. قد يدخل النظام في حالة غير مستقرة، ويتم الإبلاغ عن العطل بعد فترة طويلة، مما يُخفي السبب الحقيقي للعطل.
  • قد تتعطل برامج التشغيل التي تعمل بشكل صحيح في الظروف العادية في حالات نادرة واستثنائية، وقد لا تساعد تقنيات الاختبار التقليدية في اكتشاف سلوك برامج التشغيل في الحالات الشاذة.

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

التحليل الثابت

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

تقنيات المترجم

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

ثمة نهج آخر يتمثل في استخدام الترجمة على مستوى أعلى (MC) . [ 3 ] قد تُوسّع المترجمات الفوقية المُصممة لهذا الغرض وظائف المترجمات بإضافة أدوات فحص وتحسين خفيفة الوزن خاصة بالنظام. يجب على مطوري النظام كتابة هذه الإضافات بلغة برمجة عالية المستوى وربطها ديناميكيًا بالمترجمات لإجراء تحليل ثابت دقيق.

التحقق من نموذج البرمجيات

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

تستخدم أداة SDV (مدقق برامج التشغيل الثابتة) [ 5 ] من مايكروسوفت التحليل الثابت لبرامج تشغيل أجهزة ويندوز. يستخدم محرك التحليل الخلفي SLAM التحقق من النموذج والتنفيذ الرمزي للتحقق الثابت أثناء الترجمة. تُحدد القواعد التي يجب على برامج التشغيل مراعاتها لكل واجهة برمجة تطبيقات (API) بلغة SLIC (لغة مواصفات فحص الواجهات)، وهي لغة شبيهة بلغة C. يكتشف محرك التحليل جميع المسارات التي قد تؤدي إلى انتهاكات قواعد استخدام واجهة برمجة التطبيقات، ويُعرض كمسارات أخطاء على مستوى المصدر من خلال شفرة المصدر لبرنامج التشغيل. داخليًا، يُجرّد المحرك شفرة C إلى برنامج منطقي ومجموعة من الشروط، وهي القواعد التي يجب مراعاتها في هذا البرنامج. ثم يستخدم التحقق الرمزي من النموذج [ 6 ] للتحقق من صحة الشروط في البرنامج المنطقي.

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

يُعدّ Avinux [ 9 ] أداةً أخرى تُسهّل التحليل التلقائي لمحركات أجهزة Linux، وهو مبنيٌّ على مدقق النماذج المحدود CBMC . [ 10 ] توجد طرق لتحديد موقع العطل، حيث تُعيد أدوات فحص النماذج هذه سلسلة طويلة من أمثلة العدادات، ويصعب تحديد موقع العطل بدقة. [ 11 ]

تحليل وقت التشغيل

يُجرى تحليل البرنامج الديناميكي بتشغيل البرنامج مع مدخلات اختبار كافية لإنتاج سلوكيات مثيرة للاهتمام. يُعدّ Safe Drive [ 12 ] نظامًا منخفض التكلفة للكشف عن انتهاكات سلامة النوع في برامج تشغيل الأجهزة والتعافي منها. وبإجراء تغييرات بنسبة 4% فقط على شفرة المصدر لبرامج تشغيل شبكة Linux، تمكنوا من تطبيق Safe Drive وتوفير حماية واستعادة أفضل لنواة Linux. مشروع مشابه يستخدم الأجهزة لعزل برامج تشغيل الأجهزة عن النواة الرئيسية هو Nook [ 13 ] . يضعون برامج تشغيل الأجهزة في نطاق حماية منفصل للأجهزة يُسمى "nooks"، ولديهم إعدادات أذونات منفصلة لكل صفحة، مما يضمن عدم تعديل برنامج التشغيل للصفحات التي ليست ضمن نطاقه، ولكنه يستطيع قراءة جميع بيانات النواة لأنها تشترك في نفس مساحة العناوين.

ومن الأعمال المشابهة في هذا المجال، العمل على الاستعادة التلقائية لأنظمة التشغيل نتيجةً لأعطال برامج التشغيل. يُعدّ نظام التشغيل Minix 3 [ 14 ] نظامًا قادرًا على عزل الأعطال الرئيسية، واكتشاف العيوب، واستبدال المكونات المعطلة فورًا.

توليف برنامج تشغيل الجهاز

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

لغات تحديد الواجهات

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

تتيح لغة Devil [ 15 ] تعريفًا عالي المستوى للاتصال بالجهاز. تُعبّر مكونات الجهاز عن نفسها كمنافذ إدخال/إخراج وسجلات مُرتبطة بالذاكرة. تُحوّل هذه المواصفات بعد ذلك إلى مجموعة من وحدات الماكرو C التي يمكن استدعاؤها من كود برنامج التشغيل، مما يُزيل الخطأ الذي قد يرتكبه المبرمج أثناء كتابة الدوال منخفضة المستوى. أما لغة NDL [ 16 ] فهي تطوير للغة Devil، حيث تصف برنامج التشغيل من حيث واجهة التشغيل الخاصة به. تستخدم NDL صيغة تعريف واجهة Devil، وتتضمن مجموعة من تعريفات السجلات، وبروتوكولات الوصول إلى هذه السجلات، ومجموعة من دوال الجهاز. تُترجم دوال الجهاز بعد ذلك إلى سلسلة من العمليات على تلك الواجهة. لإنشاء برنامج تشغيل جهاز، يجب أولًا كتابة وظائف برنامج التشغيل بلغات مواصفات الواجهة هذه، ثم استخدام مُترجم برمجي يُولّد كود برنامج التشغيل منخفض المستوى.

لغة HAIL (لغة واجهة الوصول إلى الأجهزة) [ 17 ] هي لغة أخرى لتحديد مواصفات برامج تشغيل الأجهزة الخاصة بمجال معين. يحتاج مطور برنامج التشغيل إلى كتابة ما يلي.

  1. وصف خريطة التسجيل، الذي يصف سجلات الجهاز المختلفة وحقول البتات من ورقة بيانات الجهاز.
  2. وصف نطاق العناوين للوصول إلى الحافلة.
  3. إنشاء نسخة من الجهاز في النظام المحدد.
  4. المواصفات الثابتة، التي تقيد الوصول إلى الجهاز.

يقوم مُترجم HAIL بأخذ هذه المدخلات وترجمة المواصفات إلى كود C.

التصميم المشترك للأجهزة والبرامج

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

توليف برنامج التشغيل المستقل

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

تأخذ أداة Termite [ 19 ] ثلاثة مواصفات لإنشاء برنامج التشغيل.

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

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

قام فريق RevNIC [ 20 ] بجهد اختراق مثير للاهتمام ، حيث يقوم بإنشاء آلة حالة برنامج تشغيل من خلال الهندسة العكسية لبرنامج تشغيل موجود، وذلك لإنشاء برامج تشغيل آمنة وقابلة للنقل بين المنصات الجديدة. ولإجراء الهندسة العكسية لبرنامج التشغيل، يقوم الفريق بالتنصت على عمليات الإدخال/الإخراج للأجهزة عن طريق تنفيذ برنامج التشغيل باستخدام عمليات تنفيذ رمزية وملموسة. تُغذى مخرجات عملية التنصت إلى مُركِّب، يقوم بدوره بإعادة بناء مخطط تدفق التحكم لبرنامج التشغيل الأصلي من هذه المسارات المتعددة، بالإضافة إلى قالب البرنامج الأساسي لفئة الجهاز المقابلة. وباستخدام هذه الأساليب، قام الباحثون بنقل بعض برامج تشغيل Windows الخاصة بواجهات الشبكة إلى أنظمة تشغيل Linux وأنظمة تشغيل مضمنة أخرى.

نقد

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

خاتمة

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

مراجع

  1. ↑ أرتشانا غاناباثي، فيجي غاناباثي، وديفيد باترسون. " تحليل أعطال نواة نظام التشغيل ويندوز إكس بي ". في وقائع مؤتمر إدارة أنظمة التثبيت الكبيرة لعام 2006.
  2. ↑ أ. تشو، ج. يانغ، ب. تشيلف، س. هالم، و د. إنجلر. دراسة تجريبية لأخطاء أنظمة التشغيل. في SOSP، 2001
  3. ↑ إنجلر، داوسون، وتشيلف، بنجامين، وشو، آندي، وهاليم، سيث. " التحقق من قواعد النظام باستخدام امتدادات المترجم الخاصة بالنظام والمكتوبة من قبل المبرمج ". في وقائع المؤتمر الرابع حول تصميم وتنفيذ أنظمة التشغيل، 2000
  4. ↑ جالا، رانجيت وماجومدار، روباك. “فحص نموذج البرنامج”. في المسح الحسابي ACM. 2009
  5. ↑ توماس بول، إيلا بونيموفا، بايرون كوك، فلاديمير ليفين، جاكوب ليشتنبرغ، كون ماكغارفي، بوهوس أوندروسيك، سريرام راجاماني، وعبد الله أستونر. " تحليل ثابت شامل لبرامج تشغيل الأجهزة "، في مجلة SIGOPS لأنظمة التشغيل، المجلد 40، 2006.
  6. ↑ ماكميلان، كينيث ل. "التحقق من النموذج الرمزي". دار نشر كلوير الأكاديمية، 1993.
  7. ^ توماس أ. هينزنجر، رانجيت جالا، روباك ماجومدار، وجريجوار سوتري. " التحقق من البرنامج باستخدام BLAST ". في سبين، 2003.
  8. ↑ توماس أ. هينزينجر، رانجيت جالا، روباك ماجومدار، وجريجوار سوتري. "التجريد الكسول"، في مؤتمر ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة، 2002.
  9. ↑ هـ. بوست، و. كوشلين. "دمج التحليل الثابت للتحقق من برامج تشغيل أجهزة لينكس". في المؤتمر الدولي السادس حول الأساليب الرسمية المتكاملة، 2007.
  10. ↑ إدموند كلارك، ودانيال كرونينج، وفلافيو ليردا. "أداة للتحقق من برامج ANSI-C". في TACAS، 2004
  11. ↑ توماس بول، ومايور نايك، وسريرام ك. راجاماني. "من العرض إلى السبب: تحديد موقع الأخطاء في آثار الأمثلة المضادة". إشعارات ACM SIGPLAN، 2003.
  12. ↑ فينغ تشو، جيريمي كوندت، زاكاري أندرسون، إيليا باغراك، روب إينالز، ماثيو هارن، جورج نيكولا، وإريك بروير. " SafeDrive: ملحقات آمنة وقابلة للاسترداد باستخدام تقنيات قائمة على اللغة ". في المؤتمر السابع لـ OSDI، 2006.
  13. ↑ مايكل م. سويفت، ستيفن مارتن، هنري م. ليفي، وسوزان ج. إيغرز. " نوكس: بنية لبرامج تشغيل الأجهزة الموثوقة ". في المؤتمر العاشر لجمعية ACM SIGOPS، 2002.
  14. ↑ جوريت ن. هيردر، هربرت بوس، بن غراس، فيليب هومبورغ، وأندرو س. تانينباوم. " MINIX 3: نظام تشغيل عالي الموثوقية، ذاتي الإصلاح ". في SIGOPS Oper. Syst. Rev. 40، 2006.
  15. ↑ فابريس ميريون، لوران ريفيير، شارل كونسيل، رينو مارليه، وجيل مولر. " الشيطان: لغة تعريف واجهة برمجة الأجهزة ". في وقائع المؤتمر الرابع حول تصميم وتنفيذ أنظمة التشغيل، المجلد 4، 2000.
  16. ↑ كريستوفر إل. كونواي وستيفن أ. إدواردز. " NDL: لغة خاصة بالمجال لبرامج تشغيل الأجهزة ". إشعارات ACM SIGPLAN 39، 2004.
  17. ↑ ج. صن، و. يوان، م. كالاهالا، ون. إسلام. " HAIL: لغة للوصول السهل والصحيح إلى الأجهزة ". في وقائع مؤتمر ACM حول البرمجيات المدمجة، 2005.
  18. ↑ فيليس بالارين وآخرون. " التصميم المشترك للأجهزة والبرمجيات للأنظمة المدمجة. نهج POLIS ." دار نشر كلوير الأكاديمية، 1997.
  19. ↑ ليونيد ريزيك، بيتر تشاب، إيهور كوز، إتيان لو سوير، وجيرنوت هايزر. "التوليف التلقائي لبرامج تشغيل الأجهزة باستخدام Termite". في وقائع الندوة الثانية والعشرين لجمعية ACM حول مبادئ أنظمة التشغيل، 2009.
  20. ↑ فيتالي تشيبونوف وجورج كانديا. " الهندسة العكسية لبرامج تشغيل الأجهزة الثنائية باستخدام RevNIC ". المؤتمر الخامس لجمعية ACM SIGOPS/EuroSys، 2010.
  21. ↑ عاصم كاداف ومايكل إم. سويفت "فهم برامج تشغيل الأجهزة الحديثة" في وقائع المؤتمر السابع عشر لجمعية الحوسبة الآلية حول الدعم المعماري للغات البرمجة وأنظمة التشغيل