Geri Dön

Runtime checking of refinement for concurrent software components

Koşut-zamanlı yazılım bileşenleri için çalışma zamanı arıtma denetimi

PDF İndir

  1. Tez No: 182090
  2. Yazar: TAYFUN ELMAS
  3. Danışmanlar: YRD. DOÇ. DR. SERDAR TAŞIRAN
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2005
  8. Dil: İngilizce
  9. Üniversite: Koç Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: Belirtilmemiş.

Ö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 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

Özet (Çeviri)

In this thesis, we present a runtime technique for checking that a con-currently accessed data structure implementation, such as a file system orthe storage management module of a database, conforms to an executablespecification that contains an atomic method per data structure operation.The specification can be provided separately or a non-concurrent, ?atom-ized? interpretation of the implementation can serve as the specification.The technique consists of two phases. In the first phase, the implementationis instrumented in order to record information into a log during execution.In the second, a separate verification thread uses the logged information todrive an instance of the specification 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 verification method thatprovides a significant improvement over testing for concurrent programs.We formalize conformance to a specification using the notion of refine-ment: Each trace of the implementation must be equivalent to some trace ofthe specification. Among the novel features of our work are two variationson the definition of refinement appropriate for runtime checking: I/O andview refinement. These definitions were motivated by our experience withindustrial-scale concurrent data structure implementations in the Boxwoodproject, a novel storage infrastructure. I/O and view refinement checkingwere implemented as a verification tool named VYRD (VerifYing concurrentprograms by Runtime Refinement-violation Detection). VYRD was appliedto the verification 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

  1. Tez No

    143362

    Monitoring and checking of discrete event simulations

    Kesikli olayların benzetimleri üzerinde izleme ve kontrol

    BUKET ULU

    Yüksek Lisans

    İngilizce

    İngilizce

    2003

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. HALİT OĞUZTÜZÜN

    DOÇ. DR. SİNAN KAYALIGİL

  2. Tez No

    68517

    Applicability of geostatistical and fractal techniques for characterizing and deriving reservoir grid-block values for numerical simulation

    Jeoistatiksel ve fraktal tekniklerinin sayısal simülasyonda kullanılarak rezervuar blok değerlerinin hesaplanması ve krakterizasyonu için uygulanabilirliği

    BURAK YETEN

    Yüksek Lisans

    İngilizce

    İngilizce

    1997

    Petrol ve Doğal Gaz MühendisliğiOrta Doğu Teknik Üniversitesi

    Petrol ve Doğal Gaz Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. FEVZİ GÜMRAH

  3. Tez No

    39281

    RSA algoritmasını kullanan şifreleme/deşifreleme yazılımının tasarımı

    Data encyption/decryption methods and software design of RSA algorithm

    METİN ERHAN

    Yüksek Lisans

    Türkçe

    Türkçe

    1993

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    DOÇ.DR. BÜLENT ÖRENCİK

  4. Tez No

    8593

    A Parallel programing language and its runtime environment

    Başlık çevirisi yok

    REŞAT ENİS AKBABA

    Yüksek Lisans

    İngilizce

    İngilizce

    1990

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolHacettepe Üniversitesi

    Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı

    PROF. DR. ALİ SAATÇİ

  5. Tez No

    104330

    Simülasyonların etkileşimli olarak çalışması ve HLA

    Interoperable simulations and HLA

    AHMET ZENGİN

    Yüksek Lisans

    Türkçe

    Türkçe

    1999

    Elektrik ve Elektronik MühendisliğiSakarya Üniversitesi

    Elektrik-Elektronik Mühendisliği Ana Bilim Dalı

    DOÇ.DR. HÜSEYİN EKİZ

Geri Dön