ผลต่างระหว่างรุ่นของ "สปิน (ซอฟต์แวร์)"

'''สปิน''' (SPIN) คือเครื่องมือสำหรับ[[การตรวจสอบโมเดล|ตรวจสอบโมเดล]][[ซอฟต์แวร์]] พัฒนาขึ้นโดยทีมซึ่งนำโดย[[เจอราร์ด เจ. โฮลซ์แมน]] (Gerard J. Holzmann) ที่[[สถาบันวิจัยเบลล์|เบลล์แล็บ]] SPIN เป็นเครื่องมือตรวจสอบบนพื้นฐานออโตมาตา (การทำงานของเครื่องมือตรวจสอบอาศัยหลักทฤษฎีออโตมาตา). ในการตรวจสอบ, ระบบเป้าหมายสำหรับการตรวจสอบเขียนบรรยายด้วย[[ภาษาโปรเมลา]] (Promela; ''Pro''cess ''Me''ta ''La''nguage) ซึ่งมีความสามารถในการบรรยายถึงแบบจำลองของ asynchronous distributed algorithms ในรูปแบบของ non-deterministic automata ส่วนคุณสมบัติที่ต้องการตรวจสอบเขียนระบุด้วยสูตร LTL ([[ตรรกศาสตร์เวลาแบบเชิงเส้น]]; Linear Temporal Logic)

ซึ่งจะถูกนำไปหาผลลบและแปลงไปสู่[[บุชิออโตมาตา]]เพื่อนำไปใช้ในกระบวนการตรวจสอบขั้นต่อไป.