SPIN模型檢查器
我們?cè)诒緯?shū)中描述的方法集中在模型檢查器SPIN的使用上。待驗(yàn)證的系統(tǒng)是在八十年代和九十年代在貝爾實(shí)驗(yàn)室開(kāi)發(fā)的，可以從網(wǎng)上免費(fèi)獲得（見(jiàn)附錄D）坷衍。該工具不斷發(fā)展注盈，多年來(lái)吸引了學(xué)術(shù)界和工業(yè)界廣泛的用戶。在撰寫(xiě)本文時(shí)斋否，SPIN是世界上使用最廣泛的邏輯模型檢查器之一梨水。
2002年，SPIN獲得了ACM（計(jì)算機(jī)協(xié)會(huì)）頒發(fā)的最負(fù)盛名的Software System Award茵臭。在獲得此獎(jiǎng)項(xiàng)時(shí)疫诽，SPIN被置于真正突破性的軟件系統(tǒng)的聯(lián)盟中，例如UNIX旦委，TeX奇徒，Smalltalk，Postscript缨硝，TCP / IP和Tcl / Tk摩钙。這個(gè)獎(jiǎng)項(xiàng)為該工具及其基礎(chǔ)技術(shù)帶來(lái)了大量額外關(guān)注。隨著所有這些發(fā)展查辩，對(duì)權(quán)威和全面的用戶指南的需求不斷增長(zhǎng)胖笛。本書(shū)就是那本指南网持。
本書(shū)中的材料既可以作為課堂教材，也可以作為自學(xué)指南长踊，供想要了解邏輯模型檢查技術(shù)背景和使用的新用戶使用功舀。本書(shū)的一個(gè)重要部分是專門(mén)為SPIN提供一套全面的參考資料，它包含了新手和有經(jīng)驗(yàn)的用戶每天都可以應(yīng)用的信息之斯。
