Runtime checking of refinement for concurrent software components

Bu tezde, dosya sistemi ya da veritabanı depolama yünetim birimi gibiokoşut zamanlı ortamda şalıştırılan bir yazılım bileşeninin şalıştırılabilir birs cs s csbelirtime uygunluˇunu denetlemek işin bir şalışma zamanı denetleme tekniˇig c cs gsunulmaktadır. Belirtim her bir veri yapısı operasyonu işin atomik bir metotcsaˇlamaktadır. Belirtim gerşekleştirimden ayrı olarak saˇlanabileceˇi gibig c s g ggerşekleştirimin atomik olarak şalışacak hale getirilmiş bir versiyonu da belir-c s cs s˙tim olarak kullanılabilir. Tekniˇimiz iki aşamadan oluşmaktadır. Ilk aşamada,g s s sgerşekleştirim şalışma sırasında yürütme bilgisini bir günlüˇe kaydedecekc s cs uu u ug˙şekilde donatılır. Ikinci aşamada, ayrı bir sınama birimi günlüˇe kaydedilmişs s u ug syürütme bilgisini kullanarak belirtimin bir ürneˇini şalıştırır ve kayıtlı yürüt-uu o g cs uu˙menin belirtime ait yürütmeye uygunluˇunu denetler. Ilgili tekniˇin geneluu g guygulanabilirliˇine ve ülşeklenebilirliˇine, ayrıca denetlenen bileşenin koşutg oc g s szaman üzelliˇine ve başarımına etkisinin en aza indirilmesine ünem verilmiştir.o g s o sSonuş olarak, koşut zamanlı programlar işin standart test yüntemine ünemlic s c o oyenilikler getiren bir doˇrulama metodu geliştirilmiştir.g s sGerşekleştirimin belirtime uygunluˇu arıtma adında bir doˇruluk kri-c s g gteri olarak bişimsel-leştirilmiştir. Bu kritere güre gerşekleştirimin her birc s s o c syürütmesi işin ona denk belirtime ait bir yürütme bulunmalıdır. Yünteminuu c uu oyeni ozellikleri arasında en ünemlisi girdi/şıktı arıtma ve gürüş arıtma adındaü o c o usiki arıtma kriterinin tanımlanmasıdır. Boxwood adında endüstriyel ülşekteu ocveri yapısı gerşekleştirimleri işeren bir sistemin doˇrulanması şalışmalarıc s c g csbu tanımlara motivasyon kaynaˇı olmuştur. Girdi/şıktı arıtma ve gürüşg s c o usarıtmanın denetlenmesi VYRD (VerifYing concurrent programs by RuntimeRefinement-violation Detection) adlı doˇrulama aracı bünyesinde gerşekleşti-g u c srilmiştir. VYRD, Boxwood sisteminin, Java sınıf kütüphanesinden birkaşs uu csınıfın doˇrulanması amacıyla uygulanmıştır. Sonuşta, Boxwood sistemindeg s cdaha ünce tespit edilmeyen bir hataya ek olarak, Java sınıf kütüphanesindeo uuve test amaşlı yazılan ürneklerde daha ünceden bilinen hatalar yakalanmıştır.c o o sDeneyimler, ünerilen tekniˇin pratikte uygun bir şalışma maliyeti olduˇunuo g cs gortaya koymuştur.s