SPIN (การตรวจสอบโมเดล)

จากวิกิพีเดีย สารานุกรมเสรี

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

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. Addison Wesley, 2004. ISBN 0-321-22862-6.

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

ภาษาอื่น