Model Kontrolünün Temelleri

Biçimsel doğrulama (formal verification), toplumumuzda sayıları giderek artan kritik güvenlik alanlarında kullanılan bilgi işlem sistemlerinin doğruluğunu sağlamak için etkili bir yöntemdir. Bu uzmanlık programı; donanım, yazılım veya her ikisini birden içeren bilgi işlem sistemlerinin mantıksal doğrulanmasında kritik bir yaklaşım olan model kontrolünün (model checking) temel kavramlarını ve esaslarını tanıtmaktadır. Titiz matematiksel yöntemlere dayanan otomatik bir biçimsel doğrulama dalı olan model kontrolü, hedef sistemlerde yüksek güvenilirlik sağlamak için sıklıkla kullanılır. Bu uzmanlık programı ilk olarak, otomatik algoritmik analizin temeli olan modelleme biçimselliklerini tanıtacak ve farklı bilgi işlem sistemlerinin bu biçimselliklerde nasıl temsil edildiğini gösterecektir. İkinci olarak, zamanal mantıkları (temporal logics) tanıtacak ve model kontrolü için hedef sistemlerin doğru gereksinimlerini tanımlamak üzere farklı özellikleri kesin ve net bir şekilde tanımlamak için bunların nasıl kullanılabileceğini gösterecektir. Üçüncü olarak, doğrulanmakta olan bilgi işlem sistemlerinin modellerine karşı zamanal mantık özelliklerinin doğruluğuna karar vermek için temel grafik tabanlı model kontrol algoritmalarını tanıtacaktır. Son olarak, soyutlama yöntemlerini destekleyen eşdeğerlik teorilerini ele alacaktır.