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

จากวิกิพีเดีย สารานุกรมเสรี
Jump to navigation Jump to search

สปิน (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)

อ้างอิง[แก้]

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