يقدم هذا المساق مقدمة للتصميم ، والمواصفات، والتثبت من بروتوكولات الاتصال. يتضمن المساق المواضيع التالية: هيكلية تصميم البروتوكولات, نماذجها, والتحقق من صحتها, و متطلبات صحة البروتوكولات. كما يدرس الطالب تقنيات نمذجة البروتوكولات مثل FSM وPetri NET , الى جانب تقنيات التحقق من البروتوكولات. كما يتعرف الطالب الى لغة نمذجة مثل PROMELA الى جانب لفة وصف (SDL).
