Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/49916
| Title: | แบบจำลองเชิงรูปนัยเพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยสปิน |
| Other Titles: | Formal model for verifying UAV system's time scheduling using SPIN |
| Authors: | พันธ์เวสส์ สุขวนิช |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ อาทิตย์ ทองทักษ์ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | Wiwat.V@Chula.ac.th,wiwatv@gmail.com,wiwat@chula.ac.th Arthit.T@Chula.ac.th |
| Subjects: | อากาศยานไร้นักบิน -- การเขียนโปรแกรม ทฤษฎีเครื่องจักรคำนวณ สปิน (อากาศพลศาสตร์) Drone aircraft -- Programming Machine theory Spin (Aerodynamics) |
| Issue Date: | 2558 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | งานวิทยานิพนธ์นี้เสนอแบบจำลองเชิงรูปนัยด้วยภาษาโปรเมลา เพื่อการทวนสอบการกำหนดรายการเวลาของระบบยูเอวีด้วยเครื่องตรวจสอบแบบจำลองสปิน แบบจำลองเชิงรูปนัยที่เป็นผลลัพธ์ประกอบด้วย 5 แบบจำลองย่อย คือ แบบจำลองย่อยสัญญาณนาฬิกา แบบจำลองย่อยภารกิจ แบบจำลองย่อยภารกิจไม่อิสระ แบบจำลองย่อยการจัดกำหนดรายการเวลา และแบบจำลองย่อยเครื่องประมวลผลเอมทีแอล ทั้งนี้เพื่อให้สามารถแสดงขีดความสามารถของระบบเวลาจริงของระบบยูเอวีด้วยเช่นกัน แบบจำลองเชิงรูปนัยผลลัพธ์นี้ไม่เพียงแต่สามารถใช้เพื่อการทวนสอบการจัดกำหนดรายการเวลาการทำงานที่สอดคล้องตามเงื่อนไขของระบบเวลาจริงได้เท่านั้น แต่ยังรองรับภารกิจแบบจวบกันและรวมถึงภารกิจที่มีการประสานเวลาด้วยระบบนับเวลาภายในแบบจำลอง งานวิทยานิพนธ์นี้ยังเสนอวิธีการแปลสัญลักษณ์ตัวดำเนินการเชิงปริมาณพื้นฐานของภาษาเอมทีแอลมาเป็นสูตรภาษาแอลทีแอลเพื่อการทวนสอบระบบเวลาจริงด้วยเครื่องตรวจแบบจำลองสปินได้อย่างอัตโนมัติ |
| Other Abstract: | 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. |
| Description: | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2558 |
| Degree Name: | วิทยาศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมซอฟต์แวร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/49916 |
| URI: | http://doi.org/10.14457/CU.the.2015.1267 |
| metadata.dc.identifier.DOI: | 10.14457/CU.the.2015.1267 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5570988421.pdf | 2.85 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.