Geri Dön

Verification of BPEL specifications using model checking

BPEL tanımlamalarının model kontrol yöntemi ile doğrulanması

PDF İndir

  1. Tez No: 232646
  2. Yazar: MEHMET N. AKÇAY
  3. Danışmanlar: PROF. MEHMET UFUK ÇAĞLAYAN
  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: 2008
  8. Dil: İngilizce
  9. Üniversite: Boğaziçi Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 113

Özet

Servis Odaklı Mimari (SOA) farklı is akısları tarafından olusturulabilen ve networküzerinden dagıtılabilir servislerin yaratılması ile olusturulmaktadır. SOA Mimarisiile olusturulması hedeflenen is akısları için ise bir çok dil bulunmaktadır. BPELyakın zamanda ortaya çıkan bir spesifikasyon olmakla birlikte web servis mimarilerive is akıslarını için kolay ve uygun bir dil özelligi tasımaktadır. Dizayn asamasındaBPEL proseslerinin dogrulanması için, BPEL ile yazılmıs proseslere yazılım dogrulamayöntemleri uygulanabilir. Bu çalısma ile BPEL proseslerinin PROMELA proseslerinedönüstürülmesi ve bu dönüstürülmüs PROMELA processlerinin SPIN aracınınyardımı ile dogrulanması gerçeklestirilmistir. Bu çalısmada assign, switch, sequence,empty, while, terminate, scope, flow, throw, invoke, reply, receive, pick, wait ve faulthandlerBPEL aktiviteleri baz alınarak bir PROMELA modeli olusturulmaktadır. Budönüsümü gerçeklestirmek için BPEL2PML diye bir tool implemente edilip, olusanPROMELA spesifikasyonları üzerinde dogrulama islemleri yapılabilabilmistir. BPELproseslerinin PROMELA modellerinin olusturulmasının ardından, SPIN ile dogrulamayapılarak, negatif örnekler, onaylama bildirileri (assertions) ve hiçbir zaman ulasılamayankod parçacıkları tespit edilebilmektedir.

Özet (Çeviri)

Service Oriented Architecture(SOA) is based on creating services which can bedistributed on a network by different business flows. Business Process Execution Language(BPEL) is a recent specification language to express web service applicationsand business flows in an easier way in SOA implementations. In order to verify thecorrectness of BPEL processes during design, a number of software verification methodscan be applied to BPEL specified processes. In this paper, the translation ofBPEL process specifications into PROMELA specification language and verificationby model checking by SPIN tool are studied. By creating a model of any BPEL process,several verification steps can be applied during design time by the help of SPINtool. A subset of BPEL activities consisting of assign, switch, sequence, empty, while,terminate, scope, flow, throw, invoke, reply, receive, pick, wait, fault handlers and compensationhandlers are modeled to check and verify the processes specified by usingthese activities. With the tool created in this work, a given set of inputs consistingof BPEL source code(s), wsdl files(s) and BPEL descriptor file(s) are used to create aPROMELA model, then the model is verified by using the SPIN model checking toolfor counter claims, assertions and unreachable codes.

Benzer Tezler

  1. Tez No

    464149

    End-tidal karbondioksit ve trakeal ultrasonografinin entübasyon doğruluğunu onaylamadaki değerliliklerinin boroskop ile konfirme edilerek karşılaştırılması

    Comparing accuracy of tracheal ultrasonography and end-tidal carbondioxide in endotracheal tube placement BY confirmation with boroscope

    TUĞBA MAMAK

    Tıpta Uzmanlık

    Türkçe

    Türkçe

    2017

    İlk ve Acil YardımMarmara Üniversitesi

    Acil Tıp Ana Bilim Dalı

    DOÇ. DR. HALDUN AKOĞLU

  2. Tez No

    343047

    Dökümlerde besleyici işlevinin süreç benzeşimi ile kontrolü

    Verification of the function of feeders in castings with simulation

    HAYDAR KAHRAMAN

    Yüksek Lisans

    Türkçe

    Türkçe

    2013

    Metalurji MühendisliğiDokuz Eylül Üniversitesi

    Metalurji ve Malzeme Mühendisliği Ana Bilim Dalı

    PROF. DR. ÜMİT CÖCEN

  3. Tez No

    664878

    Ultrasonografinin renkli doppler, pulse wave, M modları kullanılarak epidural kateter yerinin doğrulanması

    Verification of epidural catheter site using color doppler, pulse wave and M-mode with ultrasound

    HAKAN ÖZKAN

    Tıpta Uzmanlık

    Türkçe

    Türkçe

    2021

    Anestezi ve ReanimasyonSağlık Bilimleri Üniversitesi

    Anesteziyoloji ve Reanimasyon Ana Bilim Dalı

    DR. ÖĞR. ÜYESİ HALİL ERKAN SAYAN

  4. Tez No

    286363

    Verification of a multicore programming library

    Bir çok çekirdekli programlama kütüphanesinin doğrulanması

    ETEM DENİZ

    Yüksek Lisans

    İngilizce

    İngilizce

    2011

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. ALPER ŞEN

  5. Tez No

    604661

    Verification of novel Wnt/B-catenin pathway targets

    Yeni Wnt/B-catenin sinyal yolağının hedeflerinin doğrulanması

    AYŞE NUR KAYABAŞI

    Yüksek Lisans

    İngilizce

    İngilizce

    2019

    BiyolojiBoğaziçi Üniversitesi

    Moleküler Biyoloji ve Genetik Ana Bilim Dalı

    DR. ÖĞR. ÜYESİ NECLA BİRGÜL İYİSON

Geri Dön