Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/80128
Title: การแปลงแผนภาพเวลาเป็นไทมด์ออโตมาตาสำหรับการจัดกำหนดการเชิงพรีเอ็มทีฟ
Other Titles: Transforming timing diagram into timed automata for preemptive scheduling
Authors: อมรัตน์ พิมโคตร
Advisors: วิวัฒน์ วัฒนาวุฒิ
Other author: จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
Issue Date: 2564
Publisher: จุฬาลงกรณ์มหาวิทยาลัย
Abstract: งานที่เกิดขึ้นพร้อมกันในระบบเรียลไทม์อาจต้องการทรัพยากรที่ใช้ร่วมกันอย่างจำกัด เช่นการใช้งานร่วมกันของ CPU เพียงตัวเดียวที่มีงานเป็นจำนวนมาก เมื่อใช้การจัดกระบวนการเชิงพรีเอ็มทีฟ ซึ่งงานที่กำลังทำงานอยู่ที่มีค่าลำดับความสำคัญต่ำกว่ามักจะถูกจัดลำดับให้อยู่ในสถานะพักการทำงานหรือสถานะโดเมน โดยงานใหม่ที่มีค่าลำดับความสำคัญสูงกว่าจะเข้ามาแทนที่ สุดท้ายจึงกลายเป็นว่างานใหม่เข้ามาทำงานแทนลำดับงานที่โดนแทรกหรือถูกพรีเอ็มทีฟไว้ก่อนหน้านี้ที่มีค่าลำดับความสำคัญต่ำกว่า งานที่มีค่าลำดับความสำคัญต่ำกว่าดังกล่าวจะเริ่มต้นทำงานอีกครั้งเพื่อดำเนินการต่อในสถานะที่ทำงานทันทีหลังจากงานที่มีค่าลำดับความสำคัญสูงกว่าได้ทำงานเสร็จสิ้น แผนภาพเวลาเป็นแผนภาพที่มีลักษณะงานเป็นอิสระต่อกัน และงานจะถูกเริ่มต้นพร้อมกัน ผลกระทบของการจัดกระบวนการเชิงพรีเอ็มทีฟเอาไว้จะมีความสัมพันธ์กันและทำให้การดำเนินของเส้นเวลาหรือไทม์ไลน์ของงานที่เกิดขึ้นพร้อมกันเหล่านี้ถูกเปลี่ยนแปลงไป กฎการจับคู่สำหรับการแปลงแผนภาพเวลาที่เป็นอิสระต่อกันเป็นไทมด์ออโตมาตาที่ได้รับการออกแบบในวิทยานิพนธ์นี้ และยังมีเครื่องมือซอฟต์แวร์ที่ได้รับการพัฒนาเพื่อแปลงไฟล์ต้นทางนำเข้าสกุลไฟล์ XML ของแผนภาพเวลาเป็นไฟล์ไทมด์ออโตมาตา สามารถจำลองแผนภาพไทมด์ออโตมาตาด้วยเครื่องมือ UPPAAL ซึ่งผลลัพธ์ของไทมด์ออโตมาตาจะแสดงกรอบเวลาโดยรวมของงานที่เกิดขึ้นพร้อมกันอันเป็นผลกระทบของการจัดกำหนดการเชิงฟรีเอ็มทีฟ การจำลองไทมด์ออโตมาตาจะจัดเตรียมตัวแปรนาฬิกาและสถานะโดเมนพิเศษเพิ่มเติม จากนั้นจึงนำไทมด์ออโตมาตาที่แปลงมาทวนสอบคุณสมบัติ TCTL ว่าการทำงานนั้นถูกต้อง เครื่องมือซอฟต์แวร์ของเราจะดำเนินการแปลงไดอะแกรมสำหรับการจัดกระบวนการเชิงพรีเอ็มทีฟ และใช้กรณีศึกษาสามกรณีเพื่อแสดงกระบวนการแปลงและการจำลองขั้นตอนกระบวนการทำงาน
Other Abstract: In the real-time system, the concurrent tasks occasionally require the limit shared resource, such as a single CPU would be shared among multiple tasks. When the preemptive scheduling is typically selected, the running task with lower priority value would be preempted into the dormant state by the new coming task with the higher priority value which would finally become the new running task instead. Then the previous preempted task with lower priority value would finally be activated back to resume the running state immediately after the end of the task with higher priority value. Given several timing diagrams of the independent tasks which would be concurrently initiated, the effects of preemptive scheduling would be concerned and cause the changing of the overall timelines of these concurrent tasks. In this thesis, the mapping rules of transforming the independent timing diagrams into timed automata are designed and a software tool is developed to transform the input XML files of the timing diagrams into the timed automata file, to be simulated with the UPPAAL timed automata simulation tool. The resulting timed automata shows the overall timelines of the input concurrent tasks under the effects of the preemptive scheduling. The clock variables and the extra dormant states are included to enable the observations of the timed automata simulation and the verification using the TCTL properties. Our software tool correctly performs the transforming of the diagrams with the preemptive scheduling and three case studies are used to demonstrate the transformation and simulation process.
Description: วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2564
Degree Name: วิทยาศาสตรมหาบัณฑิต
Degree Level: ปริญญาโท
Degree Discipline: วิศวกรรมซอฟต์แวร์
URI: http://cuir.car.chula.ac.th/handle/123456789/80128
URI: http://doi.org/10.58837/CHULA.THE.2021.964
metadata.dc.identifier.DOI: 10.58837/CHULA.THE.2021.964
Type: Thesis
Appears in Collections:Eng - Theses

Files in This Item:
File Description SizeFormat 
6170327521.pdf5.74 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.