Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Extracting data invariants from promela
Year (A.D.)
2018
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมซอฟต์แวร์
DOI
10.58837/CHULA.THE.2018.1274
Abstract
ตัวยืนยงชนิดข้อมูลเป็นข้อมูลคงที่ซึ่งจะมีค่าคงอยู่ตลอดการทำงานของโปรแกรม ซึ่งอยู่ในรูปของตัวแปรหรือเงื่อนไข ที่อยู่ในความต้องการที่ได้กำหนดไว้แสดงด้วยสูตรแอลทีแอล ซึ่งระบุความถูกต้องของการทำงานของโปรแกรมที่เกิดขึ้นในปัจจุบัน โปรแกรมซอฟต์แวร์จำนวนมากในปัจจุบันมุ่งเน้นเรื่องการปรับปรุงคุณภาพซอฟต์แวร์ ซึ่งการทวนสอบโปรแกรมซอฟต์แวร์ก็เป็นสิ่งสำคัญสำหรับองค์กร เนื่องจากการทวนสอบนั้นเป็นหนึ่งในวิธีที่ใช้ในการตรวจสอบความถูกต้องของอัลกอริทึมภายใต้การทำงานของซอฟต์แวร์ ในทางปฏิบัตินั้นการเขียนสูตรแอลทีแอลด้วยตนเองนั้นเป็นสิ่งที่ยาก และมีความซับซ้อนสำหรับโค้ดโปรแกรม โพรเมลาแตกต่างจากภาษาอื่นๆ เพราะโพรเมลาสนับสนุนโปรแกรมที่มีการทำงานหลายอย่างพร้อมกัน บางครั้งก็จะมีการทำงานที่สอดแทรกหรือคาบเกี่ยวกัน ซึ่งในการทำงานหลายอย่างพร้อมๆกัน ส่งผลให้กระทบกับตัวแปรหรือฟังก์ชันอื่นๆ ซึ่งอาจก่อให้เกิดข้อผิดพลาด ทำให้โปรแกรมทำงานได้ไม่ถูกต้อง และคนทั่วไปมักไม่ค่อยตระหนักถึงการทวนสอบความถูกต้องของค่าที่ใช้ในโปรแกรม งานวิจัยนี้จึงได้นำเสนอวิธีการแบ่งส่วนของข้อมูล เพื่อสร้างตัวยืนยงชนิดข้อมูลจากโพรเมลา โดยอยู่ในรูปของสูตรแอลทีแอลขึ้นมาช่วยในการตรวจสอบความถูกต้องในการทำงานของโปรแกรม
Other Abstract (Other language abstract of ETD)
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
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
สุขศรีบางเตย, วิสุทธิ์, "การสกัดตัวยืนยงชนิดข้อมูลจากโพรเมลา" (2018). Chulalongkorn University Theses and Dissertations (Chula ETD). 3405.
https://digital.car.chula.ac.th/chulaetd/3405