สปิน (ซอฟต์แวร์)
สปิน (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)
ประวัติ แก้
- การพัฒนา SPIN เริ่มขึ้นในปีค.ศ. 1980
- เวิร์คชอปประจำปีของ SPIN ได้ถูกจัดขึ้นตั้งแต่ปีค.ศ. 1995 เพื่อผู้ใช้, นักวิจัย, และผู้สนใจเกี่ยวกับการตรวจสอบโมเดล
- ในปีค.ศ. 2001SPIN ได้รับรางวัล System Software Award จาก ACM (Association for Computing Machinery)
อ้างอิง แก้
- Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, 2004. ISBN 0-321-22862-6.