|
การทวนสอบเชิงรูปนัยเฟรมเวิร์คเกียร์แมนสำหรับภาษาพีเอชพี |
|---|---|
| รหัสดีโอไอ | |
| Title | การทวนสอบเชิงรูปนัยเฟรมเวิร์คเกียร์แมนสำหรับภาษาพีเอชพี |
| Creator | วรัชญ์ ลีเกษม |
| Contributor | เด่นดวง ประดับสุวรรณ, ที่ปรึกษา |
| Publisher | มหาวิทยาลัยธรรมศาสตร์ |
| Publication Year | 2557 |
| Keyword | การทวนสอบเชิงรูปนัย, การคำนวณแบบภาวะพร้อมกัน, Time petri net, Formal verification, Concurrent computing |
| Abstract | เฟรมเวิร์คเกียร์แมนสำหรับภาษาพีเอชพีเป็นเฟรมเวิร์คสำหรับช่วยพัฒนาโปรแกรมประยุกต์บนเว็บให้สั่งงานแบบภาวะพร้อมกันได้ ทำให้ประสิทธิภาพของโปรแกรมประยุกต์เพิ่มขึ้น แต่เนื่องด้วยความซับซ้อนของชุดคำสั่ง ทำให้ผู้พัฒนาโปรแกรมประยุกต์ยากที่จะตรวจสอบความถูกต้องของเหตุการณ์ที่เป็นไปได้ทั้งหมดในการประมวลผลของโปรแกรมประยุกต์ ดังนั้นจึงจำเป็นที่จะต้องทวนสอบโปรแกรมประยุกต์เพื่อรับประกันความถูกต้องและความน่าเชื่อถืองานวิจัยฉบับนี้จึงนำเสนอการทวนสอบเชิงรูปนัย ด้วย Timed Trace theory เพื่อทวนสอบหา Safety และ Timing failures ของเฟรมเวิร์คเกียร์แมนสำหรับภาษาพีเอชพี ผลการทดลองแสดงให้เห็นประสิทธิภาพของวิธีการที่นำเสนอ |
