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

  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ı: 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 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. Generatörlerin otomatik senkronizasyonu

    Automatic synchronization of generators

    FİKRET YILDIRIM

    Yüksek Lisans

    Türkçe

    Türkçe

    2014

    Elektrik ve Elektronik Mühendisliğiİstanbul Teknik Üniversitesi

    Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı

    PROF. DR. SALMAN KURTULAN

  2. 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

    Türkçe

    2023

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolEskişehir Osmangazi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. AHMET YAZICI

    DOÇ. DR. METİN ÖZKAN

  3. Stochastic bitstream-based vision and learning machines

    Stokastik bit akışı tabanlı görü ve öğrenme makineleri

    SERCAN AYGÜN

    Doktora

    İngilizce

    İngilizce

    2022

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

    Elektronik ve Haberleşme Mühendisliği Ana Bilim Dalı

    PROF. DR. ECE OLCAY GÜNEŞ

  4. 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

  5. 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

    İngilizce

    2010

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

    Bilgisayar Bilimleri Ana Bilim Dalı

    YRD. DOÇ. DR. FEZA BUZLUCA

    DR. OKAN TOPÇU

    YRD. DOÇ. DR. YUNUS EMRE SELÇUK