แบบจำลองเชิงรูปนัยเพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยสปิน

พันธ์เวสส์ สุขวนิช

dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ	en_US
dc.contributor.advisor	อาทิตย์ ทองทักษ์	en_US
dc.contributor.author	พันธ์เวสส์ สุขวนิช	en_US
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	en_US
dc.date.accessioned	2016-11-30T05:39:22Z
dc.date.available	2016-11-30T05:39:22Z
dc.date.issued	2558	en_US
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/49916
dc.description	วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2558	en_US
dc.description.abstract	งานวิทยานิพนธ์นี้เสนอแบบจำลองเชิงรูปนัยด้วยภาษาโปรเมลา เพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยเครื่องตรวจสอบแบบจำลองสปิน แบบจำลองเชิงรูปนัยที่เป็นผลลัพธ์ประกอบด้วย 5 แบบจำลองย่อย คือ แบบจำลองย่อยสัญญาณนาฬิกา แบบจำลองย่อยภารกิจ แบบจำลองย่อยภารกิจไม่อิสระ แบบจำลองย่อยการจัดกำหนดรายการเวลา และแบบจำลองย่อยเครื่องประมวลผลเอมทีแอล ทั้งนี้เพื่อให้สามารถแสดงขีดความสามารถของระบบเวลาจริงของระบบยูเอวีด้วยเช่นกัน แบบจำลองเชิงรูปนัยผลลัพธ์นี้ไม่เพียงแต่สามารถใช้เพื่อการทวนสอบการจัดกำหนดรายการเวลาการทำงานที่สอดคล้องตามเงื่อนไขของระบบเวลาจริงได้เท่านั้น แต่ยังรองรับภารกิจแบบจวบกันและรวมถึงภารกิจที่มีการประสานเวลาด้วยระบบนับเวลาภายในแบบจำลอง งานวิทยานิพนธ์นี้ยังเสนอวิธีการแปลสัญลักษณ์ตัวดำเนินการเชิงปริมาณพื้นฐานของภาษาเอมทีแอลมาเป็นสูตรภาษาแอลทีแอลเพื่อการทวนสอบระบบเวลาจริงด้วยเครื่องตรวจแบบจำลองสปินได้อย่างอัตโนมัติ	en_US
dc.description.abstractalternative	A formal model for verifying UAV system's time scheduling is proposed in this thesis. The formal model is written in Promela and verified in SPIN model checker. Our resulting formal model consists of five submodels - Ticking submodel, Task submodel, Dependent task submodel, Scheduler submodel and MTL engine submodel, in order to cope with the real-time behavioral capability of the UAV system. The resulting formal model satisfactorily provides the real-time behavioral specification of not only the time scheduling, but also the concurrency and inner clock signal synchronization of the tasks. This thesis also proposes the automatic translating scheme of the basic MTL's quantitative operators into LTL formula as to suit the verification of the real-time system using SPIN model checker.	en_US
dc.language.iso	th	en_US
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	en_US
dc.relation.uri	http://doi.org/10.14457/CU.the.2015.1267
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	en_US
dc.subject	อากาศยานไร้นักบิน -- การเขียนโปรแกรม
dc.subject	ทฤษฎีเครื่องจักรคำนวณ
dc.subject	สปิน (อากาศพลศาสตร์)
dc.subject	Drone aircraft -- Programming
dc.subject	Machine theory
dc.subject	Spin (Aerodynamics)
dc.title	แบบจำลองเชิงรูปนัยเพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยสปิน	en_US
dc.title.alternative	Formal model for verifying UAV system's time scheduling using SPIN	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.email.advisor	Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th	en_US
dc.email.advisor	Arthit.T@Chula.ac.th	en_US
dc.identifier.DOI	10.14457/CU.the.2015.1267