Yazılımda Biçimsel Yöntemler
Biçimsel yöntemler, yazılımın belirtimi, geliştirilmesi ve doğrulanması süreçlerine matematiksel mantığı uygulamakta olup, bir sistemin özelliklerinin yalnızca test edilmek yerine kanıtlanmasına olanak tanımaktadır.
Tanım
Biçimsel yöntemler, yazılım sistemlerini belirtmek, geliştirmek ve doğrulamak için matematiksel temelli tekniklerdir; bu tekniklerde belirtimler biçimsel dillerde ifade edilmekte ve özellikler kanıt veya kapsamlı durum keşfi yoluyla belirlenmektedir.
Kapsam
Bu konu, Z, B ve TLA+ gibi biçimsel belirtim dillerini; program doğruluğu hakkında akıl yürütmek için aksiyomatik semantik ve Hoare mantığını; sonlu durumlu ve eşzamanlı sistemleri doğrulamak için model denetimini; teorem kanıtlamayı ve kanıt yardımcılarını; ve biçimsel yöntemlerin güvenlik ve emniyet açısından kritik yazılımlarda kullanımını kapsamaktadır.
Temel sorular
- Yazılım davranışı biçimsel bir dilde nasıl açıkça belirtilebilir?
- Bir programın doğruluğu, bir belirtime göre nasıl kanıtlanır?
- Model denetimi, sonlu durumlu ve eşzamanlı sistemleri kapsamlı bir şekilde nasıl doğrular?
- Biçimsel yöntemlerin maliyetleri ve faydaları, kullanımlarını nerede haklı çıkarır?
Temel kuramlar
- Hoare mantığı ve aksiyomatik semantik
- Hoare, program yapılarının doğruluğunun aksiyomlar ve çıkarım kuralları ile ifade edildiği, önkoşullar ve sonkoşullar mantığını tanıtmıştır; bu, programların belirtimlerini karşıladığını kanıtlamak için bir temel sağlamaktadır.
- Model denetimi
- Model denetimi, zamansal mantık özelliklerini doğrulamak için sonlu durumlu bir modelin erişilebilir durumlarını otomatik ve kapsamlı bir şekilde keşfetmekte, test etme ile muhtemelen gözden kaçacak kilitlenmeleri ve ihlalleri tespit etmektedir.
Klinik önem
Biçimsel yöntemler, doğruluğun mevcut en güçlü güvencesini sağlamakta ve arızanın kabul edilemez olduğu havacılık elektroniği, demiryolu sinyalizasyonu, güvenlik protokolleri ve donanım gibi alanlarda uygulanmaktadır; ancak maliyetleri nedeniyle genellikle büyük sistemlerin tamamından ziyade kritik bileşenlerle sınırlı kalmaktadır.
Kanıt ve kılavuzlar
Endüstriyel uygulamalara yönelik araştırmalar, biçimsel yöntemlerin emniyet açısından kritik alanlardaki başarılı uygulamalarını belgelemekte ve DO-178C ile Common Criteria gibi standartlar, biçimsel teknikleri en yüksek güvence seviyelerinde tanımaktadır.
Tarihçe
Program doğrulama, 1960'ların sonlarında Floyd ve Hoare tarafından kurulmuştur; model denetimi ise 1980'lerin başlarında Clarke, Emerson ve Sifakis tarafından geliştirilmiştir (bir Turing Ödülü kazanmışlardır) ve o zamandan beri araçlar ve kanıt yardımcıları, biçimsel doğrulamayı kritik sistemler için endüstriyel kullanıma taşımıştır.
Tartışmalar
- Biçimsel yöntemlerin ölçeklenebilirliği ve maliyeti
- Süregelen bir tartışma, biçimsel yöntemlerin büyük endüstriyel yazılımlara ekonomik olarak ölçeklenip ölçeklenemeyeceği üzerinedir; otomasyon ve hafif biçimsel yöntemlerdeki gelişmeler uygulanabilirliği genişletmiş olsa da, büyük sistemlerin tam doğrulaması maliyetli olmaya devam etmektedir.
Öne çıkan isimler
- C. A. R. Hoare
- Edsger Dijkstra
- Edmund Clarke
- Leslie Lamport
İlgili konular
Temel eserler
- hoare1969
- clarke1999
- woodcock2009
Sıkça sorulan sorular
- Biçimsel yöntemler test etmenin yerini alır mı?
- Genellikle hayır. Biçimsel yöntemler bir model veya belirtim hakkında güçlü güvenceler sağlamaktadır, ancak varsayımlar, ortam ve modellenmemiş yönler yine de test edilmeyi gerektirmektedir; pratikte ikisi birbirini tamamlamakta olup, biçimsel yöntemler en kritik özelliklere odaklanmaktadır.
- Biçimsel yöntemler neden her yerde kullanılmamaktadır?
- Çoğu yazılım için haklı çıkarılması zor olan uzmanlık ve çaba gerektirmektedirler; bu tür yazılımlarda test etme, daha düşük maliyetle yeterli güven sağlamaktadır. Biçimsel yöntemler, arızanın sonuçlarının yatırımı haklı çıkaracak kadar ciddi olduğu yerlerde yoğunlaşmaktadır.