En tehlikeli sistem kusurlarından bazıları, tasarımın kendisi analiz edilebilir bir sistem olarak ele alınırsa kod yazılmadan önce tespit edilebilir. Hillel Wayne’in sunumunun odağında bu konu yer alıyor: Biçimsel yöntemlerin ilkelerinin gelecekteki sistemleri incelemeye ve esneklik, eşzamanlılık ve arıza sorunlarını operasyonel hatalara dönüşmeden önce keşfetmeye nasıl yardımcı olduğunu açıklıyor.
Wayne, «görev yürütücüsü» olarak adlandırdığı basitleştirilmiş bir örnekle başlıyor: Sistem görevin tamamlanıp tamamlanmadığını kontrol ediyor, ardından tamamlandı işareti koyuyor ve daha sonra görevi yürütüyor. Sıralama mantıklı görünüyor, ancak yürütme sırasında bir arıza meydana geldiğinde bozuluyor. Görev tamamlandı olarak kaydedildikten sonra yeniden deneme yapılabilir ve böylece görev gerçekte hiç yürütülmez. Tamamlanma kaydı yürütme sonrasına alındığında ise başka bir sorun ortaya çıkıyor: Eşzamanlı iki yürütücü, ikisinden biri tamamlanma kaydı tutmadan önce aynı görevi iki kez yürütebilir.
Bu yalnızca teorik bir sorun değildir; sunum bunu paket gönderim sistemlerinin siparişi iki kez gönderebilmesi, planlama sistemlerinin aynı randevuyu iki kişiye ayırabilmesi ve uygulama yükleme mekanizmalarının talebin tekrarlanması durumunda bozucu bir davranışa girebilmesi gibi örneklerle ilişkilendiriyor.
«Doğru»nun ne anlama geldiğini tanımlayarak başlayın
Wayne, sistem gereksinimlerinin ikili özellikler biçiminde ifade edilmesini öneriyor: Özellikler ya doğru ya da yanlış olmalı. Örneğin görevin birden fazla yürütülmemesi, kötü bir şeyin gerçekleşmesini engelleyen bir güvenlik özelliğidir; görevin en az bir kez yürütülmesi ise istenen bir şeyin gerçekleşmesini güvence altına alan bir canlılık özelliğidir.
Sunum, özelliklerin güç bakımından eşit olmadığını vurguluyor. Saniyede 10.000 sorguyu işleyebilen bir sistem, saniyede iki sorgu işleme özelliğini otomatik olarak karşılar; ancak bunun tersi geçerli değildir. Bu nedenle güçlü bir özelliğin geçilmesi, daha zayıf özelliklerden oluşan bir kümenin doğruluğuna kanıt olabilirken, daha zayıf bir özelliğin başarısız olması hatanın kaynağını daraltmaya yardımcı olur. Wayne bu fikri test piramidiyle ilişkilendiriyor: Çok sayıda birim testi, hatayı teşhis etmede sınırlı sayıdaki uçtan uca testten daha yararlı olabilir.
Basitleştirilmiş model temel sorunu ortaya çıkarır
Wayne, sistemi tüm ayrıntılarıyla temsil etmek yerine gerekli en az durum bilgisini içeren soyut bir model oluşturmayı öneriyor: Algoritmanın mevcut aşaması, görevin tamamlandı olarak işaretlenip işaretlenmediği ve kaç kez yürütüldüğü. Bu, başarısızlık ve yeniden deneme durumları da dahil olmak üzere olası durumların ve sistemin izleyebileceği yolların keşfedilmesini sağlar.
Biçimsel yöntemlerde bu model ve özellikler mantıksal formüller kullanılarak kodlanabilir ve model denetleyicileri ile SMT çözücüleri gibi araçlarla incelenebilir. Ancak sunumdaki pratik fikir, bu araçların doğrudan kullanılmasını gerektirmiyor; mühendis, olası durumları ve geçişleri izleyerek aynı düşünme biçimini benimseyebilir.
Eşzamanlılık ve arızalarda «hasım» faktörü
Wayne, kullanıcı girdisi, eşzamanlılık, rastgelelik, zaman aşımı ve sunucu kesintileri gibi her belirsizlik kaynağının, daima mümkün olan en kötü sonucu seçen bir «hasım» olarak düşünülmesini öneriyor. Sistem sonsuza kadar yeniden deneme yapabiliyorsa bu hasım her seferinde arızayı seçer; bu da başarı teorik olarak mümkün olsa bile canlılık özelliğinin güvence altında olmadığını ortaya çıkarır.
Ayrıca iki eşzamanlı yürütücünün bulunmasının, bazı değişkenlerin her süreç için yerel, diğerlerinin ise sistemle dış dünya arasında paylaşılan değişkenler olarak temsil edilmesini gerektirdiğini açıklıyor. Farklı yürütme sıraları keşfedilerek, her bir yürütücü tek başına hatasız göründüğünde bile görevin iki kez yürütüldüğü bir duruma ulaşılabilir.
Varsayımlar tasarımın bir parçasıdır
Sistemin doğruluğu yalnızca özelliklerine değil, çalıştığı ortama ilişkin varsayımlara da bağlıdır. Bir tasarım, sürecin hiçbir zaman başarısız olmayacağı yönünde güçlü bir varsayım gerektirebilirken, başka bir tasarım başarısızlığın sınırlı sayıda meydana gelmesi durumunda çalışabilir. Wayne, adımların yeniden sıralanmasının canlılık varsayımlarını azaltabileceğini, ancak aynı anda yalnızca bir yürütücünün bulunmasını güvence altına alma gereksinimi gibi güvenlik gereksinimlerini artırabileceğini belirtiyor.
Çalışma ortamı değiştiğinde durum da değişir. Güçlü tutarlılığa sahip bir veritabanına güvenip daha sonra nihai tutarlılığa geçmek, sistemin kodu değişmese bile daha önce doğru olan özellikleri güvence altından çıkarabilir. Bu nedenle hizmet sağlayıcının veya veritabanının varsayımları dış ayrıntılar olarak görülmemeli; bunlar tasarımın doğruluğu için doğrudan koşullardır.
Pratikte ne değişir?
Yöntemin pratik değeri, testlerin yerine geçmesinde veya her projede biçimsel araçların kullanılmasını savunmasında değil, tasarım sorularını daha kesin hâle getirmesindedir: Olası durumlar nelerdir? Olayların en kötü sıralaması nedir? Gerçekte neyi kontrol ediyoruz? Ekibin güvence altına alamadığı varsayımlar hangileridir? Gerekli özellik ne kadar güçlüyse veya ortam ne kadar öngörülemezse sistemin tasarımı da o kadar karmaşık olmalı ya da gerekli özellik gevşetilmelidir; örneğin «tüm iletileri işleme» koşulu, «iletileri işleme veya ölü ileti kuyruğuna gönderme» koşuluna dönüştürülebilir.
Wayne bu fikirleri, biçimsel yöntemlerden türetilen düşünme araçları olarak sunuyor; bunları mühendislik yargısının hazır bir alternatifi olarak görmüyor. Her sistemde açık kalan soru, kullanılan modelin ve varsayımların ne kadar doğru olduğudur. Bir durum gözden kaçırılırsa veya ekip ortamın güvence altına almadığı bir davranışı varsayarsa analiz, gerçek sisteme benzemeyen bir modelin doğruluğunu kanıtlayabilir.