สปิน (ซอฟต์แวร์)

สปิน (SPIN) คือเครื่องมือสำหรับซอฟต์แวร์ พัฒนาขึ้นโดยทีมซึ่งนำโดย (Gerard J. Holzmann) ที่ SPIN เป็นเครื่องมือตรวจสอบบนพื้นฐานออโตมาตา (การทำงานของเครื่องมือตรวจสอบอาศัยหลักทฤษฎีออโตมาตา). ในการตรวจสอบ, ระบบเป้าหมายสำหรับการตรวจสอบเขียนบรรยายด้วย (Promela; Process Meta Language) ซึ่งมีความสามารถในการบรรยายถึงแบบจำลองของ asynchronous distributed algorithms ในรูปแบบของ non-deterministic automata ส่วนคุณสมบัติที่ต้องการตรวจสอบเขียนระบุด้วยสูตร LTL (; Linear Temporal Logic) ซึ่งจะถูกนำไปหาผลลบและแปลงไปสู่เพื่อนำไปใช้ในกระบวนการตรวจสอบขั้นต่อไป. นอกจากจะเป็นเครื่องมือสำหรับตรวจสอบโมเดลแล้ว SPIN ยังสามารถใช้เป็นเพื่อจำลองวิถีการรันที่เป็นไปได้ของระบบ และแสดงผลเป็นสายของการรันระบบได้.

SPIN แตกต่างไปจากเครื่องมือตรวจสอบโมเดลอื่นๆตรงที่มันไม่ได้กระทำการตรวจสอบด้วยตัวของมันเอง แต่จะสร้างโค้ดภาษา C ขึ้นมาเป็นตัวตรวจสอบสำหรับโมเดลเป้าหมายแต่ละอัน. ซึ่งเทคนิคนี้ช่วยประหยัดหน่วยความจำและทำให้การตรวจสอบมีประสิทธิภาพ และนอกจากนั้นยังทำให้การเพิ่มเติม/แก้ไขโมเดล โดยเพิ่มเติม/แก้ไขบางส่วนของโค้ดผลลัพธ์ที่ได้จาก SPIN. SPIN ยังมีทางเลือกที่ช่วยให้กระบวนการตรวจสอบมีความรวดเร็วมากยิ่งขึ้นและประหยัดหน่วยความจำมากยิ่งขึ้น อาธิเช่น:

• การลดลำดับบางส่วน (partial order reduction) ;
• การบีบอัดสเตท (state compression) ;
• การแฮชบิทสเตท (bitstate hashing) คือ แทนที่จะเก็บทั้งหมดของสเตทก็จัดเก็บเพียงแค่แฮชโค้ดในบิทฟิลด์. เทคนิคนี้ช่วยลดการใช้หน่วยความจำได้อย่างมากแต่ก็ต้องแลกด้วยการสูญเสียความสมบูรณ์ไป;
• การบับคับความเท่าเทียมแบบหละหลวม (weak fairness enforcement)

ประวัติ

1. การพัฒนา SPIN เริ่มขึ้นในปีค.ศ. 1980
2. เวิร์คชอปประจำปีของ SPIN ได้ถูกจัดขึ้นตั้งแต่ปีค.ศ. 1995 เพื่อผู้ใช้, นักวิจัย, และผู้สนใจเกี่ยวกับการตรวจสอบโมเดล
3. ในปีค.ศ. 2001SPIN ได้รับรางวัล System Software Award จาก ACM (Association for Computing Machinery)

อ้างอิง

• Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual. , 2004. .

แหล่งข้อมูลอื่น

• SPIN website