التحقق من النماذج باستخدام المنطق الزمني

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

• تحديد سلوك الزمن الخطي ووصف خصائصه باستخدام منطق الزمن الخطي (LTL)
• شرح أساسيات فحص نموذج LTL
• تحديد الخصائص باستخدام منطق شجرة الحساب (CTL)
• شرح أساسيات فحص نموذج CTL وإصداره الرمزي

• مهارات حاسوب وإنترنت أساسية
• القدرة على قراءة التعليمات وإتمام الأنشطة البسيطة باللغة الإنجليزية