Runtime checking of refinement for concurrent software components
Koşut-zamanlı yazılım bileşenleri için çalışma zamanı arıtma denetimi
- Tez No: 182090
- Danışmanlar: YRD. DOÇ. DR. SERDAR TAŞIRAN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2005
- Dil: İngilizce
- Üniversite: Koç Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 129
Özet
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 RuntimeReï¬nement-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
Özet (Çeviri)
In this thesis, we present a runtime technique for checking that a con-currently accessed data structure implementation, such as a ï¬le system orthe storage management module of a database, conforms to an executablespeciï¬cation that contains an atomic method per data structure operation.The speciï¬cation can be provided separately or a non-concurrent, ?atom-ized? interpretation of the implementation can serve as the speciï¬cation.The technique consists of two phases. In the ï¬rst phase, the implementationis instrumented in order to record information into a log during execution.In the second, a separate veriï¬cation thread uses the logged information todrive an instance of the speciï¬cation and to check whether the logged exe-cution conforms to it. We paid special attention to the general applicabilityand scalability of the techniques and to minimizing their concurrency andperformance impact. The result is a lightweight veriï¬cation method thatprovides a signiï¬cant improvement over testing for concurrent programs.We formalize conformance to a speciï¬cation using the notion of reï¬ne-ment: Each trace of the implementation must be equivalent to some trace ofthe speciï¬cation. Among the novel features of our work are two variationson the deï¬nition of reï¬nement appropriate for runtime checking: I/O andview reï¬nement. These deï¬nitions were motivated by our experience withindustrial-scale concurrent data structure implementations in the Boxwoodproject, a novel storage infrastructure. I/O and view reï¬nement checkingwere implemented as a veriï¬cation tool named VYRD (VerifYing concurrentprograms by Runtime Reï¬nement-violation Detection). VYRD was appliedto the veriï¬cation of Boxwood, Java class libraries. It was able to detectpreviously unnoticed subtle concurrency bugs in Boxwood, the known bugsin the Java class libraries and manually constructed examples. Experimentalresults indicate that our techniques have modest computational cost.
Benzer Tezler
- Generatörlerin otomatik senkronizasyonu
Automatic synchronization of generators
FİKRET YILDIRIM
Yüksek Lisans
Türkçe
2014
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
PROF. DR. SALMAN KURTULAN
- Verification and validation of robotic systems's safety
Robotik sistemlerin emniyetinin doğrulanması ve onaylanması
ZEKERİYYA DEMİRCİ
Yüksek Lisans
Türkçe
2023
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolEskişehir Osmangazi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. AHMET YAZICI
DOÇ. DR. METİN ÖZKAN
- Stochastic bitstream-based vision and learning machines
Stokastik bit akışı tabanlı görü ve öğrenme makineleri
SERCAN AYGÜN
Doktora
İngilizce
2022
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiElektronik ve Haberleşme Mühendisliği Ana Bilim Dalı
PROF. DR. ECE OLCAY GÜNEŞ
- Monitoring and checking of discrete event simulations
Kesikli olayların benzetimleri üzerinde izleme ve kontrol
BUKET ULU
Yüksek Lisans
İngilizce
2003
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. HALİT OĞUZTÜZÜN
DOÇ. DR. SİNAN KAYALIGİL
- Verifying the interface compliance of federates using pre- and postconditions of RTI services
Çalışma zamanı altyapısı (RTI) servislerinin ön ve son koşullarını kullanarak federe arayüz uyumluluğunun geçerlenmesi
VİJDAN KIZILAY
Yüksek Lisans
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Bilimleri Ana Bilim Dalı
YRD. DOÇ. DR. FEZA BUZLUCA
DR. OKAN TOPÇU
YRD. DOÇ. DR. YUNUS EMRE SELÇUK