【名人推薦】我第一次翻開這本書時(shí)，立刻被這本書的覆蓋范圍之廣所深深打動(dòng)，它覆蓋了規(guī)約和建模、演繹驗(yàn)證、模型檢驗(yàn)、進(jìn)程代數(shù)、程序測(cè)試、狀態(tài)與消息序列圖。除了對(duì)每個(gè)方法進(jìn)行了相當(dāng)深入的介紹以外，本書還討論了應(yīng)當(dāng)在何時(shí)選取何種方法以及在選擇這些方法時(shí)所必須做出的權(quán)衡。書中結(jié)合當(dāng)前工具，使用很多具有挑戰(zhàn)性的實(shí)例來(lái)說(shuō)明各種技術(shù)。我還沒(méi)看見過(guò)其他任何覆蓋同樣內(nèi)容的書籍能達(dá)到如此的深度。同時(shí)，本書描述了應(yīng)用形式化方法的過(guò)程：從建模和規(guī)約開始，然后選擇一個(gè)合適的驗(yàn)證技術(shù)，最后測(cè)試程序。這些知識(shí)在實(shí)踐中是十分必要的，但是卻很少在軟件工程的課本里面出現(xiàn)。我確信這本書將會(huì)取得巨大的成功。我向所有對(duì)軟件可靠性問(wèn)題感興趣的讀者強(qiáng)烈推薦這本書?！?Edmund M. Clarke教授圖靈獎(jiǎng)獲得者，卡內(nèi)基-梅隆大學(xué)【內(nèi)容簡(jiǎn)介】用于創(chuàng)建可靠軟件的形式化方法一直處于不斷的開發(fā)和改進(jìn)之中。最近，人們對(duì)于形式化方法工具的重要組成有了更深入的理解，從軟硬件開發(fā)業(yè)界逐漸接受可靠性工具這一點(diǎn)就可以體現(xiàn)出來(lái)。本書介紹了各種能解決軟件可靠性問(wèn)題的方法。理想情況下，形式化方法應(yīng)該用起來(lái)直觀，學(xué)起來(lái)簡(jiǎn)潔、快速，對(duì)開發(fā)過(guò)程的影響微乎其微。本書對(duì)各種方法進(jìn)行了比較，揭示了它們各自的優(yōu)點(diǎn)和缺點(diǎn)，同時(shí)緊扣自動(dòng)機(jī)理論和邏輯這兩個(gè)主題。在盡可能減少背景知識(shí)介紹的前提下，本書向非專家讀者描述了多種技術(shù)，并且針對(duì)軟件工程領(lǐng)域的研究人員和專業(yè)人士介紹了一些高級(jí)技術(shù)。本書主題和特點(diǎn)：？ 集中介紹目前常用的重要軟件可靠性方法，并將它們互作比較，這些方法包括：演繹驗(yàn)證、自動(dòng)驗(yàn)證、測(cè)試和進(jìn)程代數(shù)？ 為具體項(xiàng)目的軟件選擇過(guò)程提供有用信息？ 提供了大量的練習(xí)、項(xiàng)目和連續(xù)性的實(shí)例，方便讀者學(xué)習(xí)形式化方法并能夠親手使用這些工具？ 介紹了支持形式化方法的數(shù)學(xué)原理？ 對(duì)于該領(lǐng)域未來(lái)的研究方向，以及開發(fā)新方法和改進(jìn)現(xiàn)有技術(shù)提出了有益的見解
作者簡(jiǎn)介
Doron A. Peled 以色列巴依蘭大學(xué)（BarIlanUniversity）計(jì)算機(jī)科學(xué)系教授。主要研究領(lǐng)域?yàn)椴l(fā)理論、形式化驗(yàn)證、形式化規(guī)約、編程語(yǔ)言語(yǔ)義、模型檢驗(yàn)、有限自動(dòng)機(jī)、軟件測(cè)試、時(shí)序邏輯等。著有多部書籍和論文。王林章南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系副教授、碩士生導(dǎo)師，南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室主任助理。主要研究方向?yàn)檐浖こ?、新型軟件測(cè)試方法、模型驅(qū)動(dòng)軟件測(cè)試與驗(yàn)證、自動(dòng)化軟件測(cè)試工具。目前面向本科生、研究生講授軟件工程、軟件體系結(jié)構(gòu)、軟件測(cè)試等課程。
鄂公網(wǎng)安備 42010302001612號(hào) 