版權(quán)
為了區(qū)分商品恶阴，很多名稱被制造商和銷售商聲明為商標(biāo)。如果這些名稱出現(xiàn)在本書(shū)中焦匈，并且Addison-Wesley出版社意識(shí)到這是一個(gè)商標(biāo)聲明，則該名稱首字母大寫或全部大寫昵仅。
作者和出版商在編寫本書(shū)時(shí)已經(jīng)小心謹(jǐn)慎累魔，但不作任何明示或暗示的保證够滑，對(duì)錯(cuò)誤或遺漏不承擔(dān)任何責(zé)任。對(duì)于因使用本書(shū)包含的信息或程序而產(chǎn)生的偶然或間接損失彰触，我們不承擔(dān)任何責(zé)任。
在訂購(gòu)按照數(shù)量進(jìn)行特價(jià)銷售時(shí)况毅，出版商提供這本書(shū)的折扣。 獲取更多資訊么鹤，請(qǐng)聯(lián)系：
U.S. Corporate and Government Sales: (800) 382-3419
corpsales@pearsontechgroup.com
如需在美國(guó)境外銷售味廊，請(qǐng)聯(lián)系：
International Sales: (317) 581-3793
international@pearsontechgroup.com
訪問(wèn)Addison-Wesley出版社的網(wǎng)站：awprofessional.com
美國(guó)國(guó)會(huì)圖書(shū)館編目出版數(shù)據(jù)
Holzmann, Gerard J.
The Spin model checker: primer and reference manual / Gerard J. Holzmannp. cm
Includes bibliographical references and index.
ISBN 0-321-22862-6
1.Systems engineering––Mathematical models. 2.Computer programs––Testing. I. Title.
TA168.H65 2003
620'.001'171––dc22
2003057704
CIP
Copyright ? 2004 Lucent Technologies Inc., Bell Laboratories.
保留所有權(quán)利。未經(jīng)出版商事先同意柠新，不得以任何形式或通過(guò)任何手段（電子，機(jī)械登颓，影印红氯，錄制或其他方式）復(fù)制，存儲(chǔ)在檢索系統(tǒng)中或傳播本出版物的任何部分痢甘。本書(shū)在美國(guó)影印。 同時(shí)在加拿大出版塞栅。
本書(shū)由作者編寫，設(shè)計(jì)和排版作烟，同時(shí)隸屬于貝爾實(shí)驗(yàn)室的計(jì)算科學(xué)研究中心砾医。他目前隸屬于美國(guó)宇航局噴氣推進(jìn)實(shí)驗(yàn)室/加州理工學(xué)院的可靠軟件實(shí)驗(yàn)室拿撩。
有關(guān)獲得使用此作品中材料的許可的信息如蚜，請(qǐng)?zhí)峤徽?qǐng)求：
Pearson Education, Inc.
Rights and Contracts Department
75 Arlington Street, Suite 300
Boston, MA 0211
Fax: (617) 848-7047
文字印在再生紙上
第一次印刷影暴，2003年9月
