Yazılım için Model Denetimi
Model denetimi, bir sistemin modelinin zamansal mantık spesifikasyonunu karşılayıp karşılamadığını, erişilebilir durumlarını kapsamlı bir şekilde inceleyerek otomatik olarak doğrulamaktadır.
Tanım
Model denetimi, bir sistemin sonlu durumlu bir modeli ve bir zamansal mantık spesifikasyonu verildiğinde, spesifikasyonun sağlanıp sağlanmadığını kapsamlı bir şekilde denetleyen ve sağlanmıyorsa bir karşı örnek izi üreten otomatik bir doğrulama tekniğidir.
Kapsam
Bu konu, sonlu durumlu ve eşzamanlı sistemlerin zamansal mantık özelliklerine (güvenlik ve canlılık) karşı otomatik doğrulanmasını, durum patlaması sorununu ve bununla mücadele tekniklerini (ikili karar diyagramları ile sembolik temsil, kısmi sıralı indirgeme, soyutlama), SAT/SMT ile sınırlı model denetimini ve yazılım için karşı örnek güdümlü soyutlama iyileştirmesini kapsamaktadır.
Temel sorular
- Bir özellik, tüm erişilebilir durumlar keşfedilerek nasıl doğrulanabilir?
- Durum patlaması sorunu nedir ve nasıl hafifletilir?
- Sembolik ve sınırlı yöntemler model denetimini nasıl ölçeklendirir?
- Sonsuz durumlu yazılım sistemleri sonlu modellere nasıl soyutlanır?
Temel kuramlar
- Zamansal mantık model denetimi
- Clarke, Emerson ve Sistla ile bağımsız olarak Queille ve Sifakis, sonlu durumlu eşzamanlı sistemleri zamansal mantık spesifikasyonlarına karşı otomatik olarak denetlemek için algoritmalar sunmuşlardır.
- Sembolik model denetimi
- Burch ve meslektaşları, durum kümelerini ikili karar diyagramları ile sembolik olarak temsil ederek, astronomik sayıda duruma sahip sistemlerin doğrulanmasını mümkün kılmış ve naif durum patlaması sorununu aşmışlardır.
Klinik önem
Model denetimi, donanım tasarımlarını, iletişim protokollerini ve eşzamanlı ve güvenliğe kritik yazılımları doğrulamak için kullanılmaktadır; bu alanlarda testlerin gözden kaçırdığı hassas hataları tespit etmekte ve kusurları işaret eden karşı örnekler sağlamaktadır. Otomasyonu, onu etkileşimli teorem ispatından ayırmaktadır.
Tarihçe
Pnueli'nin programlar için zamansal mantığı tanıtmasının ardından, Clarke ve Emerson ile bağımsız olarak Queille ve Sifakis, 1981-82 yılları civarında model denetimini geliştirmişlerdir; bu çalışma daha sonra bir Turing Ödülü ile tanınmıştır. İkili karar diyagramları ile sembolik model denetimi (1990'lar) ve SAT tabanlı sınırlı model denetimi, kapsamını büyük ölçüde genişletmiş ve soyutlama-iyileştirme yöntemleri onu yazılıma taşımıştır.
Tartışmalar
- Durum patlamasıyla mücadele
- Merkezi zorluk, durum sayısının sistem boyutuyla üstel olarak artmasıdır; araştırmacılar, doğrulamayı uygulanabilir kılmak için sembolik temsil, soyutlama, kısmi sıralı indirgeme ve sınırlı denetimin en iyi karışımını tartışmaktadır.
Öne çıkan isimler
- Edmund Clarke
- E. Allen Emerson
- Joseph Sifakis
- Kenneth McMillan
- Amir Pnueli
İlgili konular
Temel eserler
- clarke1986
- queille1982
- burch1992
Sıkça sorulan sorular
- Model denetimi, teorem ispatından nasıl farklılaşır?
- Model denetimi tamamen otomatiktir ve sonlu veya soyutlanmış modeller için bir sistemin durum uzayını kapsamlı bir şekilde incelerken, teorem ispatı mantıksal çıkarım kullanır (genellikle etkileşimli olarak) ve sonsuz durumlu sistemleri ele alabilmekle birlikte daha fazla insan rehberliği gerektirmektedir.
- Durum patlaması sorunu nedir?
- Bir sistem bileşen veya değişken kazandıkça erişilebilir durum sayısındaki üstel artışıdır; bu durum, naif model denetimini sınırlamakta ve sembolik, sınırlı ve soyutlama tabanlı teknikleri gerekli kılmaktadır.