Key points are not available for this paper at this time.
يقوم المؤلفون بإضفاء الطابع الرسمي على تحليل السلامة لخصائص التوقيت في الأنظمة الزمنية الحقيقية. يعتمد التحليل على منطق رسمي، RTL (منطق الزمن الحقيقي)، الذي يناسب بشكل خاص التفكير في سلوك التوقيت للأنظمة. بالنظر إلى المواصفة الرسمية لنظام ما وادعاء السلامة المراد تحليله، الهدف هو ربط ادعاء السلامة بمواصفة النظام. هناك ثلاث حالات مميزة: (1) ادعاء السلامة هو نظرية قابلة للاشتقاق من مواصفة الأنظمة؛ (2) ادعاء السلامة غير قابل للتحقيق بالنسبة لمواصفة الأنظمة؛ أو (3) نفي ادعاء السلامة قابل للتحقيق تحت ظروف معينة. تم تقديم طريقة منهجية لأداء تحليل السلامة.
درس جانهيان وآخرون (الإثنين) هذا السؤال.