版權(quán)

為了區(qū)分商品，很多名稱被制造商和銷售商聲明為商標(biāo)。如果這些名稱出現(xiàn)在本書中，并且Addison-Wesley出版社意識到這是一個商標(biāo)聲明，則該名稱首字母大寫或全部大寫。

作者和出版商在編寫本書時已經(jīng)小心謹(jǐn)慎，但不作任何明示或暗示的保證，對錯誤或遺漏不承擔(dān)任何責(zé)任。對于因使用本書包含的信息或程序而產(chǎn)生的偶然或間接損失，我們不承擔(dān)任何責(zé)任。

在訂購按照數(shù)量進(jìn)行特價銷售時，出版商提供這本書的折扣。 獲取更多資訊，請聯(lián)系：

U.S. Corporate and Government Sales: (800) 382-3419
corpsales@pearsontechgroup.com

如需在美國境外銷售，請聯(lián)系：

International Sales: (317) 581-3793
international@pearsontechgroup.com

訪問Addison-Wesley出版社的網(wǎng)站：awprofessional.com

美國國會圖書館編目出版數(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)出版商事先同意，不得以任何形式或通過任何手段（電子，機(jī)械，影印，錄制或其他方式）復(fù)制，存儲在檢索系統(tǒng)中或傳播本出版物的任何部分。本書在美國影印。 同時在加拿大出版。

本書由作者編寫，設(shè)計和排版，同時隸屬于貝爾實驗室的計算科學(xué)研究中心。他目前隸屬于美國宇航局噴氣推進(jìn)實驗室/加州理工學(xué)院的可靠軟件實驗室。

有關(guān)獲得使用此作品中材料的許可的信息，請?zhí)峤徽埱螅?/p>

Pearson Education, Inc.
Rights and Contracts Department
75 Arlington Street, Suite 300
Boston, MA 0211
Fax: (617) 848-7047

文字印在再生紙上

第一次印刷，2003年9月