การสกัดตัวยืนยงชนิดข้อมูลจากโพรเมลา

วิสุทธิ์ สุขศรีบางเตย

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/74197

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ	-
dc.contributor.author	วิสุทธิ์ สุขศรีบางเตย	-
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	-
dc.date.accessioned	2021-06-28T07:49:21Z	-
dc.date.available	2021-06-28T07:49:21Z	-
dc.date.issued	2561	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/74197	-
dc.description	วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2561	en_US
dc.description.abstract	ตัวยืนยงชนิดข้อมูลเป็นข้อมูลคงที่ซึ่งจะมีค่าคงอยู่ตลอดการทำงานของโปรแกรม ซึ่งอยู่ในรูปของตัวแปรหรือเงื่อนไข ที่อยู่ในความต้องการที่ได้กำหนดไว้แสดงด้วยสูตรแอลทีแอล ซึ่งระบุความถูกต้องของการทำงานของโปรแกรมที่เกิดขึ้นในปัจจุบัน โปรแกรมซอฟต์แวร์จำนวนมากในปัจจุบันมุ่งเน้นเรื่องการปรับปรุงคุณภาพซอฟต์แวร์ ซึ่งการทวนสอบโปรแกรมซอฟต์แวร์ก็เป็นสิ่งสำคัญสำหรับองค์กร เนื่องจากการทวนสอบนั้นเป็นหนึ่งในวิธีที่ใช้ในการตรวจสอบความถูกต้องของอัลกอริทึมภายใต้การทำงานของซอฟต์แวร์ ในทางปฏิบัตินั้นการเขียนสูตรแอลทีแอลด้วยตนเองนั้นเป็นสิ่งที่ยาก และมีความซับซ้อนสำหรับโค้ดโปรแกรม โพรเมลาแตกต่างจากภาษาอื่นๆ เพราะโพรเมลาสนับสนุนโปรแกรมที่มีการทำงานหลายอย่างพร้อมกัน บางครั้งก็จะมีการทำงานที่สอดแทรกหรือคาบเกี่ยวกัน ซึ่งในการทำงานหลายอย่างพร้อมๆกัน ส่งผลให้กระทบกับตัวแปรหรือฟังก์ชันอื่นๆ ซึ่งอาจก่อให้เกิดข้อผิดพลาด ทำให้โปรแกรมทำงานได้ไม่ถูกต้อง และคนทั่วไปมักไม่ค่อยตระหนักถึงการทวนสอบความถูกต้องของค่าที่ใช้ในโปรแกรม งานวิจัยนี้จึงได้นำเสนอวิธีการแบ่งส่วนของข้อมูล เพื่อสร้างตัวยืนยงชนิดข้อมูลจากโพรเมลา โดยอยู่ในรูปของสูตรแอลทีแอลขึ้นมาช่วยในการตรวจสอบความถูกต้องในการทำงานของโปรแกรม	en_US
dc.description.abstractalternative	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	en_US
dc.language.iso	th	en_US
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	en_US
dc.relation.uri	http://doi.org/10.58837/CHULA.THE.2018.1274	-
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	en_US
dc.subject	การเขียนโปรแกรม (คอมพิวเตอร์)	-
dc.subject	คอมพิวเตอร์อัลกอริทึม	-
dc.subject	Computer programming	-
dc.subject	Computer algorithmsComputer programming	-
dc.title	การสกัดตัวยืนยงชนิดข้อมูลจากโพรเมลา	en_US
dc.title.alternative	Extracting data invariants from promela	en_US
dc.type	Thesis	en_US
dc.degree.name	วิทยาศาสตรมหาบัณฑิต	en_US
dc.degree.level	ปริญญาโท	en_US
dc.degree.discipline	วิศวกรรมซอฟต์แวร์	en_US
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย	en_US
dc.identifier.DOI	10.58837/CHULA.THE.2018.1274	-
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

Show simple item record