SPIN (การตรวจสอบโมเดล) - วิกิพีเดีย

# 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.

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

- SPIN website

ดึงข้อมูลจาก "http://th.wikipedia.org../../../s/p/i/SPIN_%28%E0%B8%81%E0%B8%B2%E0%B8%A3%E0%B8%95%E0%B8%A3%E0%B8%A7%E0%B8%88%E0%B8%AA%E0%B8%AD%E0%B8%9A%E0%B9%82%E0%B8%A1%E0%B9%80%E0%B8%94%E0%B8%A5%29_aa54.html".

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

##### Views

- บทความ
- อภิปราย
- รุ่นปัจจุบัน

##### ค้นหา

##### ภาษาอื่น

- English