Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/74197
| Title: | การสกัดตัวยืนยงชนิดข้อมูลจากโพรเมลา |
| Other Titles: | Extracting data invariants from promela |
| Authors: | วิสุทธิ์ สุขศรีบางเตย |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Subjects: | การเขียนโปรแกรม (คอมพิวเตอร์) คอมพิวเตอร์อัลกอริทึม Computer programming Computer algorithmsComputer programming |
| Issue Date: | 2561 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | ตัวยืนยงชนิดข้อมูลเป็นข้อมูลคงที่ซึ่งจะมีค่าคงอยู่ตลอดการทำงานของโปรแกรม ซึ่งอยู่ในรูปของตัวแปรหรือเงื่อนไข ที่อยู่ในความต้องการที่ได้กำหนดไว้แสดงด้วยสูตรแอลทีแอล ซึ่งระบุความถูกต้องของการทำงานของโปรแกรมที่เกิดขึ้นในปัจจุบัน โปรแกรมซอฟต์แวร์จำนวนมากในปัจจุบันมุ่งเน้นเรื่องการปรับปรุงคุณภาพซอฟต์แวร์ ซึ่งการทวนสอบโปรแกรมซอฟต์แวร์ก็เป็นสิ่งสำคัญสำหรับองค์กร เนื่องจากการทวนสอบนั้นเป็นหนึ่งในวิธีที่ใช้ในการตรวจสอบความถูกต้องของอัลกอริทึมภายใต้การทำงานของซอฟต์แวร์ ในทางปฏิบัตินั้นการเขียนสูตรแอลทีแอลด้วยตนเองนั้นเป็นสิ่งที่ยาก และมีความซับซ้อนสำหรับโค้ดโปรแกรม โพรเมลาแตกต่างจากภาษาอื่นๆ เพราะโพรเมลาสนับสนุนโปรแกรมที่มีการทำงานหลายอย่างพร้อมกัน บางครั้งก็จะมีการทำงานที่สอดแทรกหรือคาบเกี่ยวกัน ซึ่งในการทำงานหลายอย่างพร้อมๆกัน ส่งผลให้กระทบกับตัวแปรหรือฟังก์ชันอื่นๆ ซึ่งอาจก่อให้เกิดข้อผิดพลาด ทำให้โปรแกรมทำงานได้ไม่ถูกต้อง และคนทั่วไปมักไม่ค่อยตระหนักถึงการทวนสอบความถูกต้องของค่าที่ใช้ในโปรแกรม งานวิจัยนี้จึงได้นำเสนอวิธีการแบ่งส่วนของข้อมูล เพื่อสร้างตัวยืนยงชนิดข้อมูลจากโพรเมลา โดยอยู่ในรูปของสูตรแอลทีแอลขึ้นมาช่วยในการตรวจสอบความถูกต้องในการทำงานของโปรแกรม |
| Other Abstract: | Data invariants are constant data that could persist data or control program integrity. They have to be true throughout the program execution. LTL formulae is referring to time for specifying correctness requirement of program, it is possible to prove the correctness of the function for executable program Many software programs emphasize to improve software quality by verify software program to help organizations. Verification is one of most effective way that provides a correctness of intended algorithms underlying a software with respect to a certain formal specification or property In practice, writing the LGL formula manually is so difficult and complicate for program source code. Promela is meant to be difference from other languages that it supports the concurrency. Conceptually a program may be thought of as a collection of threads. Several threads may compute values of the same variable. Many of these threads may interleaving others. Some people are not aware the correctness of the value to define program by LTL formulae. This thesis proposes the method to extracting data invariants for generate LTL formulae to verify correctness program |
| Description: | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561 |
| Degree Name: | วิทยาศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมซอฟต์แวร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/74197 |
| URI: | http://doi.org/10.58837/CHULA.THE.2018.1274 |
| metadata.dc.identifier.DOI: | 10.58837/CHULA.THE.2018.1274 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| En_5870962321_Wisut Su.pdf | 2.48 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.