我們可以為某些平臺提供自包含的二進制文件，如果您無法在您的平臺上編譯源代碼一铅，請與我們聯(lián)系陕贮。 系統(tǒng)要求 目前，MCMAS已根據(jù)以下配置進行編譯： ...

SPIN模型檢查器 我們在本書中描述的方法集中在模型檢查器SPIN的使用上潘飘。待驗證的系統(tǒng)是在八十年代和九十年代在貝爾實驗室開發(fā)的肮之，可以從網(wǎng)上免費...

邏輯模型檢查 我們用于檢查軟件設(shè)計正確性的方法在大多數(shù)工程學(xué)科上都是標(biāo)準(zhǔn)的掉缺。該方法稱為模型檢查。當(dāng)軟件本身無法徹底驗證時戈擒，我們可以構(gòu)建一個簡化的...

前言 "If you don't know where you're going, it doesn't really matter which...

版權(quán) 為了區(qū)分商品眶明，很多名稱被制造商和銷售商聲明為商標(biāo)。如果這些名稱出現(xiàn)在本書中峦甩，并且Addison-Wesley出版社意識到這是一個商標(biāo)聲明赘来，...