Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/52201
| Title: | การทวนสอบการปฏิสัมพันธ์ของบีเพลสำหรับทอสกา |
| Other Titles: | Verification of BPEL interaction for TOSCA |
| Authors: | วรัญช์ เจริญสุข |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th |
| Subjects: | คลาวด์คอมพิวติง Cloud computing |
| Issue Date: | 2559 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | คลาวด์ออเคสเทรชันช่วยการจัดเรียงและประสานการทำงานร่วมกันของกระบวนการธุรกิจ เพื่อให้สามารถบริหารจัดการทรัพยากรและการประมวลผล ได้คล่องตัวและมีประสิทธิภาพ มาตรฐานของคลาวด์ออเคสเทรชัน จะถูกนำมาเป็นแนวทางในการพัฒนาเครื่องมือสนับสนุน และทอสกาเป็นมาตรฐานแบบเปิดสำหรับคลาวด์ที่สำคัญ ซึ่งได้ถูกแนะนำและอนุมัติโดยองค์กรโอเอซิส ทำให้จากการที่นำทอสกามาใช้จะทำให้ผู้ให้บริการคลาวด์สามารถกำหนดโครงสร้างและอธิบายการทำงานร่วมกันของบริการที่สัมพันธ์เหล่านั้นด้วยมาตรฐานกลางที่สามารถนำการออกแบบดังกล่าวไปใช้งานข้ามแพลตฟอร์มหรือโครงสร้างพื้นฐานที่ต่างกันได้ อย่างไรก็ตาม การทวนสอบการออกแบบของคลาวด์ออเคสเทรชันด้วยมาตรฐานทอสกาจึงเป็นสิ่งสำคัญ เพื่อให้แน่ใจและเตือนนักออกแบบเมื่อพบข้อผิดพลาดที่ไม่เป็นไปตามคุณสมบัติความปลอดภัย วิทยานิพนธ์นี้จึงนำเสนอทางเลือกในการทำการทวนสอบแบบจำลองเชิงรูปนัยของการออกแบบคลาวด์ออเคสเทรชัน ด้วยการทาบกระบวนการทางธุรกิจที่อธิบายด้วยบีเพล ซึ่งสื่อสารผ่านเว็บเซอร์วิส ลงบนมาตรฐานทอสกาที่อธิบายคลาวด์ออเคสเทรชัน และสร้างเป็นแบบจำลองเชิงรูปนัย นอกจากนั้นการทาบกันยังรวมถึงจุดเชื่อมต่อและความสอดคล้องกันของพฤติกรรมในระดับระบบบริการที่ประกอบด้วยส่วนงานธุรกิจที่ประสานงานกัน ในวิทยานิพนธ์เล่มนี้จะมุ่งเน้นไปที่การปฏิสัมพันธ์ของบีเพลของคลาวด์ออเคสเทรชันด้วยเครื่องมือสนับสนุนการทวนสอบ และกำหนดเงื่อนไขการทวนสอบตามรูปแบบแอลทีแอลลงในแบบจำลองเชิงรูปนัยด้วยภาษาโพเมลา เพื่อนำไปทวนสอบด้วยเครื่องมือสปิน |
| Other Abstract: | Cloud orchestration helps arrange and coordinate the business processes or workflows to obtain the ultimate and efficient virtual computing resources management. The cloud orchestration standards are introduced to guide the development of the orchestration tools. TOSCA is an important new open cloud standard, introduced and approved by OASIS. Using TOSCA, the cloud providers are able to define the interoperable description of services and their relationships, and to enable the portability and automated management across cloud platforms and infrastructures. However the verification of the cloud orchestration design with TOSCA is still crucial to ensure and alert when the safety properties of the cloud design are violated. We propose an alternative mean to do the formal verification of the cloud orchestration design by superimposing the relevant BPEL of web services over the existing TOSCA description of a cloud orchestration. The resulting formal model of the superimposition between BPEL and TOSCA defines not only the orchestration of the web services but also their service interfaces and the corresponding high level behaviors of the services. In this thesis, the BPEL interaction of the cloud orchestration are focused only and defined using the linear temporal logic formula. Our formal model is correctly written in Promela and formally verified using model checker SPIN. |
| Description: | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2559 |
| Degree Name: | วิทยาศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมซอฟต์แวร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/52201 |
| URI: | http://doi.org/10.58837/CHULA.THE.2016.1000 |
| metadata.dc.identifier.DOI: | 10.58837/CHULA.THE.2016.1000 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5670954121.pdf | 4.91 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.