Program Analizi ve Doğrulaması
Program analizi ve doğrulaması, programların ne yaptığını anlamak, hataları tespit etmek veya yazılımın spesifikasyonunu karşıladığını kanıtlamak için titiz teknikler kullanmaktadır.
Tanım
Program analizi, bir programın davranışının özelliklerinin tüm girdilerde çalıştırılmadan otomatik olarak türetilmesidir; program doğrulaması ise bir programın resmi bir spesifikasyonu karşıladığının ispat veya kapsamlı kontrol yoluyla belirlenmesidir.
Kapsam
Bu alan, programlar hakkında otomatik ve yarı otomatik akıl yürütmeyi kapsamaktadır: statik analiz ve veri akışı teknikleri, sağlam yaklaşımlar için birleştirici bir çerçeve olarak soyut yorumlama (abstract interpretation), sonlu durumlu ve eşzamanlı sistemlerin model kontrolü ve ispat yardımcıları ile tümdengelimli doğrulama. Bu alan, sağlamlığı, kesinlik ve karar verilebilirlik arasındaki dengeyi ve güvenilir yazılım oluşturmak için bu yöntemlerin kullanımını ele almaktadır.
Alt konular
Temel sorular
- Program özellikleri, karar verilemezliğe rağmen nasıl sağlam bir şekilde hesaplanabilmektedir?
- Analizler, kesinliği ölçeklenebilirlikle nasıl dengelemektedir?
- Bir sistemin doğruluğu, test edilmek yerine ne zaman kapsamlı bir şekilde kontrol edilebilmektedir?
- Tam fonksiyonel doğruluk ispatları nasıl inşa edilmekte ve makine tarafından kontrol edilmektedir?
Temel kuramlar
- Soyut yorumlama (Abstract interpretation)
- Cousot ve Cousot, sağlam statik analizlerin bir programın semantiğinin yaklaşımları olarak türetildiği, birçok analizi birleştiren ve sağlamlıklarını garanti eden kafes-teorik bir çerçeve oluşturmuştur.
- Zamansal mantık model kontrolü
- Clarke, Emerson ve Sistla, sonlu durumlu eşzamanlı sistemlerin, durum uzayını kapsamlı bir şekilde keşfederek zamansal mantık spesifikasyonlarına karşı otomatik olarak nasıl doğrulanabileceğini göstermiştir.
- Mekanize uçtan uca doğrulama
- Leroy'nin doğrulanmış derleyicisi, gerçekçi yazılımların bir ispat yardımcısı ile doğru olduğunun kanıtlanabileceğini ve derlemenin program davranışını koruduğuna dair makine tarafından kontrol edilmiş bir garanti taşıdığını göstermektedir.
Klinik önem
Program analizi ve doğrulaması, büyük ölçekte hataları ve güvenlik açıklarını bulan, emniyet açısından kritik havacılık ve otomotiv yazılımlarını sertifikalandıran ve makine tarafından kontrol edilmiş derleyiciler ile işletim sistemi çekirdekleri üreten araçların temelini oluşturmaktadır. Bu yöntemler, doğruluğu test tabanlı güvenceden kanıtlanabilir garantilere dönüştürmektedir.
Tarihçe
Veri akışı analizi, 1970'lerde optimize edici derleyicilerle ortaya çıkmıştır; aynı on yılda Cousot'lar soyut yorumlamayı (abstract interpretation) tanıtmıştır. Model kontrolü, 1980'lerin başında Clarke ve Emerson aracılığıyla ve bağımsız olarak Queille ve Sifakis tarafından ortaya çıkmış, daha sonra bir Turing Ödülü kazanmıştır. 2000'li yıllar, CompCert ve seL4 gibi büyük ölçekli endüstriyel statik analiz ve mekanize doğrulama başarılarına tanıklık etmiştir.
Tartışmalar
- Analizlerin sağlamlığına karşı pratikliği
- Araç geliştiricileri, analizlerin tüm olası hataları raporlayarak tamamen sağlam olup olmayacağını ancak birçok yanlış alarma yol açma riskini taşıyıp taşımayacağını veya gürültüyü ve ölçeği azaltmak için kasıtlı olarak sağlam olmayacağını tartışmaktadır; bu, endüstriyel hata bulma araçlarını şekillendiren bir gerilimdir.
Öne çıkan isimler
- Patrick Cousot
- Radhia Cousot
- Edmund Clarke
- E. Allen Emerson
- Xavier Leroy
İlgili konular
Temel eserler
- cousot1977
- clarke1986
- leroy2009
- nielson1999
Sıkça sorulan sorular
- Statik analiz ile doğrulama arasındaki fark nedir?
- Statik analiz, tam spesifikasyonlar olmadan yaklaşık özellikleri (olası boş işaretçi referansları gibi) otomatik olarak çıkarmaktadır; doğrulama ise bir programın kesin bir resmi spesifikasyonu karşıladığını kanıtlamaktadır, bu genellikle daha fazla çaba gerektirmekte ve daha güçlü garantiler sağlamaktadır.
- Doğruluk karar verilemez ise, analiz nasıl çalışabilmektedir?
- Analizler, sağlam yaklaşımlar hesaplayarak karar verilemezliği aşmaktadır: gerçekte meydana gelemeyecek bazı olasılıkları raporlayabilirler, ancak doğruladıkları özelliğin gerçek bir ihlalini asla gözden kaçırmazlar.