สปิน (ซอฟต์แวร์)
สปิน (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 เพื่อผู้ใช้, นักวิจัย และผู้สนใจเกี่ยวกับการตรวจสอบโมเดล
- ในปี ค.ศ. 2001 SPIN ได้รับรางวัล 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.