Verification of BPEL specifications using model checking
BPEL tanımlamalarının model kontrol yöntemi ile doğrulanması
- Tez No: 232646
- Danışmanlar: PROF. MEHMET UFUK ÇAĞLAYAN
- 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: 2008
- Dil: İngilizce
- Üniversite: Boğaziçi Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- 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
- 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
2017
İlk ve Acil YardımMarmara ÜniversitesiAcil Tıp Ana Bilim Dalı
DOÇ. DR. HALDUN AKOĞLU
- 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
2013
Metalurji MühendisliğiDokuz Eylül ÜniversitesiMetalurji ve Malzeme Mühendisliği Ana Bilim Dalı
PROF. DR. ÜMİT CÖCEN
- 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
2021
Anestezi ve ReanimasyonSağlık Bilimleri ÜniversitesiAnesteziyoloji ve Reanimasyon Ana Bilim Dalı
DR. ÖĞR. ÜYESİ HALİL ERKAN SAYAN
- Verification of a multicore programming library
Bir çok çekirdekli programlama kütüphanesinin doğrulanması
ETEM DENİZ
Yüksek Lisans
İngilizce
2011
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. ALPER ŞEN
- 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
2019
BiyolojiBoğaziçi ÜniversitesiMoleküler Biyoloji ve Genetik Ana Bilim Dalı
DR. ÖĞR. ÜYESİ NECLA BİRGÜL İYİSON