การจัดรูปนัยและตรวจสอบความต้องกันของแผนภาพสถานะยูเอ็มแอลโดยใช้ซีอาร์อีและไพแคลคูลัส

Abstract

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