Arşiv ve Dokümantasyon Merkezi
Dijital Arşivi

Verification of BPEL specifications using model checking

Basit öğe kaydını göster

dc.contributor Graduate Program in Computer Engineering.
dc.contributor.advisor Çağlayan, M. Ufuk.
dc.contributor.author Akçay, Mehmet N.
dc.date.accessioned 2023-03-16T09:59:42Z
dc.date.available 2023-03-16T09:59:42Z
dc.date.issued 2008.
dc.identifier.other CMPE 2008 A33
dc.identifier.uri http://digitalarchive.boun.edu.tr/handle/123456789/12095
dc.description.abstract Service Oriented Architecture(SOA) is based on creating services which can be distributed on a network by different business flows. Business Process Execution Language (BPEL) is a recent specification language to express web service applications and business flows in an easier way in SOA implementations. In order to verify the correctness of BPEL processes during design, a number of software verification methods can be applied to BPEL specified processes. In this paper, the translation of BPEL process specifications into PROMELA specification language and verification by 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 SPIN tool. A subset of BPEL activities consisting of assign, switch, sequence, empty, while, terminate, scope, flow, throw, invoke, reply, receive, pick, wait, fault handlers and compensation handlers are modeled to check and verify the processes specified by using these activities. With the tool created in this work, a given set of inputs consisting of BPEL source code(s), wsdl files(s) and BPEL descriptor file(s) are used to create a PROMELA model, then the model is verified by using the SPIN model checking tool for counter claims, assertions and unreachable codes.
dc.format.extent 30cm.
dc.publisher Thesis (M.S.)-Bogazici University. Institute for Graduate Studies in Science and Engineering, 2008.
dc.relation Includes appendices.
dc.relation Includes appendices.
dc.subject.lcsh Web services.
dc.subject.lcsh Computer software -- Development.
dc.subject.lcsh Computer network architectures.
dc.subject.lcsh Computer architecture.
dc.title Verification of BPEL specifications using model checking
dc.format.pages xv, 98 leaves;


Bu öğenin dosyaları

Bu öğe aşağıdaki koleksiyon(lar)da görünmektedir.

Basit öğe kaydını göster

Dijital Arşivde Ara


Göz at

Hesabım