การแปลงไทมด์เพทริเน็ตให้เป็นอีเวนท์บีโดยอัตโนมัติสำหรับการทวนสอบเชิงรูปนัย

Abstract

โดยทั่วไปการออกแบบซอฟต์แวร์เป็นขั้นตอนที่สำคัญในกระบวนการพัฒนาซอฟต์แวร์ ความถูกต้องของพฤติกรรมของระบบซอฟต์แวร์แบบเรียลไทม์มีความสัมพันธ์กับเวลาของการทำงานของระบบ หากพบข้อผิดพลาดหลังจากการพัฒนาซอฟต์แวร์จะทำให้มีผลกระทบที่ต้องสูญเสียอย่างมาก จึงเป็นสิ่งสำคัญที่ต้องทำการทวนสอบแบบจำลองของการออกแบบ เพื่อหาจุดผิดพลาดก่อนที่จะลงเมื่อพัฒนาซอฟต์แวร์ วิทยานิพนธ์นี้จึงนำเสนอทางเลือกในการทวนสอบเชิงรูปนัยโดยใช้ไทมด์เพทริเน็ตในการสร้างแบบจำลองเชิงรูปนัย ซึ่งในปฏิบัติแล้วไทมด์เพทริเน็ตเป็นวิธีการเชิงรูปนัยที่ใช้สัญลักษณ์กราฟิกสำหรับจำลองโครงสร้างของระบบ ซึ่งทำให้สามารถเข้าใจพฤติกรรมของระบบได้ง่าย แต่ไทมด์เพทริเน็ตยังขาดการแสดงส่วนของข้อมูลที่ใช้ภายในระบบและยังไม่ได้มีการปรับแต่งใดๆ หากระบบมีขนาดใหญ่และมีความซับซ้อนมาก อาจจะเกิดปัญหาการระบบของสถานะได้ State explosion อีกทางเลือกของวิธีการเชิงรูปนัยพบว่าอีเวนท์บี เป็นวิธีการเชิงรูปนัยที่นิยมสำหรับการทวนสอบการทำงานของระบบโดยสนใจข้อมูลภายในระบบอีกทั้งสนับสนุนการปรับแต่งของระบบซอฟต์แวร์แบบเรียลไทม์ โดยใช้วิธีการพิสูจน์ทฤษฎีทางคณิตศาสตร์ ซึ่งจะทำให้ไม่เกิดปัญหาการระเบิดของสถานะในระหว่างการทวนสอบ อย่างไรก็ตามการเขียนอีเวนท์บีไม่ง่ายนักเนื่องจากต้องมีทักษะทางด้านคณิตศาสตร์สำหรับการเขียนอีเวนท์บีเพื่อทวนสอบระบบ งานวิทยานิพนธ์นี้จึงเสนอเครื่องมือการแปลงไทมด์เพทริเน็ตให้เป็นอีเวนท์บีโดยอัตโนมัติสำหรับการทวนสอบเชิงรูปนัย โดยสนใจแบบจำลองไทมด์เพทริเน็ตที่มีค่าน้ำหนักโทเค็นที่มีค่าเท่ากับ 1 เท่านั้น และกฎการแปลงส่วนประกอบไทมด์เพทริเน็ตให้เป็นอีเวนท์บีทั้งหมด 7 ข้อ ข้อมูลนำเข้าเครื่องมือการแปลงจะเป็นแบบจำลองไทมด์เพทริเน็ตที่อยู่ในรูปแบบแฟ้มเอกสารเอกซ์เอ็มแอล และเครื่องมือจะดำเนินการแปลงโดยใช้กฎการแปลงที่ได้นิยามขึ้นมา เพื่อแปลงแบบจำลองไทมด์เพทริเน็ตให้เป็นอีเวนท์บีได้โดยอัตโนมัติ เมื่อได้ผลลัพธ์การแปลงอีเวนท์บีเรียบร้อยแล้ว จะดำเนินการทวนสอบด้วยเครื่องมือโรดิน เพื่อตรวจสอบความถูกต้องของวิธีการแปลงโดยใช้เครื่องมือการแปลงและทวนสอบการทำงานของระบบ