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
- Verification of putative novel wnt/beta-catenin pathway targets using alternative effectors
Wnt/beta-katenin yolağının mefruz yeni hedef genlerinin alternatif efektürler kullanarak teyidi
TOLGA ASLAN
Yüksek Lisans
İngilizce
2009
BiyolojiBoğaziçi ÜniversitesiMoleküler Biyoloji ve Genetik Ana Bilim Dalı
PROF. DR. AHMET KOMAN
YRD. DOÇ. DR. NECLA BİRGÜL İYİSON
- Verification of sequencel programs using Mizar
Başlık çevirisi yok
ADEM ÖZYAVAŞ
Doktora
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolTexas Tech UniversityDr. NELSON J. RUSTHON
- Verification of SDL systems with partial order methods
SDL sistemlerinin kısmi sıralama metodları ile doğrulanması
MEHMET ALPER ŞEN
Yüksek Lisans
İngilizce
1997
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. KEMAL İNAN
- Ebu'l-Fazl Muhammed b. Ca'fer el-Herevî'nin Mefâhıru'l-Makâl fi'l-Mesâdiri ve'l-Ef'âl adlı yazma eserinin 191. varaktan sonuna kadar tahkiki
Verification of the handwritten book of Ebu?l-Fazl Muhammed b. Ca'fer el-Herevî Mefâhiru?l-Makâl fi?l-Mesâdiri ve?l-Ef'âl from 191 page to the end
UĞUR GÜLBİL
Doktora
Türkçe
2010
DilbilimSelçuk ÜniversitesiTemel İslam Bilimleri Ana Bilim Dalı
PROF. DR. TACETTİN UZUN
- Seramik sağlık gereçleri deformasyonlarının sonlu elemanlar analiziyle doğrulanması
Verification of ceramic sanitaryware deformation through finite element analysis
AYBİKE ÜRKMEZ
Yüksek Lisans
Türkçe
2018
Makine MühendisliğiEskişehir Osmangazi ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. NACİ ZAFER