Chulalongkorn University Theses and Dissertations (Chula ETD)
แบบจำลองเชิงรูปนัยเพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยสปิน
Other Title (Parallel Title in Other Language of ETD)
Formal model for verifying UAV system's time scheduling using SPIN
Year (A.D.)
2015
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Second Advisor
อาทิตย์ ทองทักษ์
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิศวกรรมซอฟต์แวร์
DOI
10.58837/CHULA.THE.2015.1156
Abstract
งานวิทยานิพนธ์นี้เสนอแบบจำลองเชิงรูปนัยด้วยภาษาโปรเมลา เพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยเครื่องตรวจสอบแบบจำลองสปิน แบบจำลองเชิงรูปนัยที่เป็นผลลัพธ์ประกอบด้วย 5 แบบจำลองย่อย คือ แบบจำลองย่อยสัญญาณนาฬิกา แบบจำลองย่อยภารกิจ แบบจำลองย่อยภารกิจไม่อิสระ แบบจำลองย่อยการจัดกำหนดรายการเวลา และแบบจำลองย่อยเครื่องประมวลผลเอมทีแอล ทั้งนี้เพื่อให้สามารถแสดงขีดความสามารถของระบบเวลาจริงของระบบยูเอวีด้วยเช่นกัน แบบจำลองเชิงรูปนัยผลลัพธ์นี้ไม่เพียงแต่สามารถใช้เพื่อการทวนสอบการจัดกำหนดรายการเวลาการทำงานที่สอดคล้องตามเงื่อนไขของระบบเวลาจริงได้เท่านั้น แต่ยังรองรับภารกิจแบบจวบกันและรวมถึงภารกิจที่มีการประสานเวลาด้วยระบบนับเวลาภายในแบบจำลอง งานวิทยานิพนธ์นี้ยังเสนอวิธีการแปลสัญลักษณ์ตัวดำเนินการเชิงปริมาณพื้นฐานของภาษาเอมทีแอลมาเป็นสูตรภาษาแอลทีแอลเพื่อการทวนสอบระบบเวลาจริงด้วยเครื่องตรวจแบบจำลองสปินได้อย่างอัตโนมัติ
Other Abstract (Other language abstract of ETD)
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.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
สุขวนิช, พันธ์เวสส์, "แบบจำลองเชิงรูปนัยเพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยสปิน" (2015). Chulalongkorn University Theses and Dissertations (Chula ETD). 70400.
https://digital.car.chula.ac.th/chulaetd/70400