You are here
Progress towards push button verification for business process execution language artifacts
- Date Issued:
- 2009
- Summary:
- Web Service Business Process Execution Language (BPEL) has become a standard language in the world of Service Oriented Architecture (SOA) for specifying interactions between internet services. This standard frees developers from low-level concerns involving platform, implementation, and versioning. These freedoms risk development of less robust artifacts that may even become part of a mission-critical system. Model checking a BPEL artifact for correctness with respect to temporal logic properties is computationally complex, since it requires enumerating all communication and synchronization amongst various services with itself. This entails modeling BPEL features such as concurrency, hierarchy, interleaving, and non-deterministic choice. The thesis will provide rules and procedures for translating these features to a veriable model written in Promela. We will use these rules to build a program which automates the translation process, bringing us one step closer to push button verification. Finally, two BPEL artifacts will be translated, manually edited, verified, and analyzed.
Title: | Progress towards push button verification for business process execution language artifacts. |
![]() ![]() |
---|---|---|
Name(s): |
Vargas, Augusto. College of Engineering and Computer Science Department of Computer and Electrical Engineering and Computer Science |
|
Type of Resource: | text | |
Genre: | Electronic Thesis Or Dissertation | |
Date Issued: | 2009 | |
Publisher: | Florida Atlantic University | |
Physical Form: | electronic | |
Extent: | xvi, 285 p. : ill. (some col.) | |
Language(s): | English | |
Summary: | Web Service Business Process Execution Language (BPEL) has become a standard language in the world of Service Oriented Architecture (SOA) for specifying interactions between internet services. This standard frees developers from low-level concerns involving platform, implementation, and versioning. These freedoms risk development of less robust artifacts that may even become part of a mission-critical system. Model checking a BPEL artifact for correctness with respect to temporal logic properties is computationally complex, since it requires enumerating all communication and synchronization amongst various services with itself. This entails modeling BPEL features such as concurrency, hierarchy, interleaving, and non-deterministic choice. The thesis will provide rules and procedures for translating these features to a veriable model written in Promela. We will use these rules to build a program which automates the translation process, bringing us one step closer to push button verification. Finally, two BPEL artifacts will be translated, manually edited, verified, and analyzed. | |
Identifier: | 502242731 (oclc), 369386 (digitool), FADT369386 (IID), fau:4273 (fedora) | |
Note(s): |
by Augusto Varas. Thesis (M.S.C.S.)--Florida Atlantic University, 2009. Includes bibliography. Electronic reproduction. Boca Raton, Fla., 2009. Mode of access: World Wide Web. |
|
Subject(s): |
Electronic commerce -- Computer programs Computer network architectures Expert systems (Computer science) Web servers -- Management Computer systems -- Verification |
|
Persistent Link to This Record: | http://purl.flvc.org/FAU/369386 | |
Use and Reproduction: | http://rightsstatements.org/vocab/InC/1.0/ | |
Host Institution: | FAU |