軟件可靠性方法

內(nèi)容概要

　　【名人推薦】
　　我第一次翻開(kāi)這本書(shū)時(shí)，立刻被這本書(shū)的覆蓋范圍之廣所深深打動(dòng)，它覆蓋了規(guī)約和建模、演繹驗(yàn)證、模型檢驗(yàn)、進(jìn)程代數(shù)、程序測(cè)試、狀態(tài)與消息序列圖。除了對(duì)每個(gè)方法進(jìn)行了相當(dāng)深入的介紹以外，本書(shū)還討論了應(yīng)當(dāng)在何時(shí)選取何種方法以及在選擇這些方法時(shí)所必須做出的權(quán)衡。書(shū)中結(jié)合當(dāng)前工具，使用很多具有挑戰(zhàn)性的實(shí)例來(lái)說(shuō)明各種技術(shù)。我還沒(méi)看見(jiàn)過(guò)其他任何覆蓋同樣內(nèi)容的書(shū)籍能達(dá)到如此的深度。
　　同時(shí)，本書(shū)描述了應(yīng)用形式化方法的過(guò)程：從建模和規(guī)約開(kāi)始，然后選擇一個(gè)合適的驗(yàn)證技術(shù)，最后測(cè)試程序。這些知識(shí)在實(shí)踐中是十分必要的，但是卻很少在軟件工程的課本里面出現(xiàn)。我確信這本書(shū)將會(huì)取得巨大的成功。我向所有對(duì)軟件可靠性問(wèn)題感興趣的讀者強(qiáng)烈推薦這本書(shū)。
　　—— Edmund M. Clarke教授
　　圖靈獎(jiǎng)獲得者，卡內(nèi)基-梅隆大學(xué)
　　【內(nèi)容簡(jiǎn)介】
　　用于創(chuàng)建可靠軟件的形式化方法一直處于不斷的開(kāi)發(fā)和改進(jìn)之中。最近，人們對(duì)于形式化方法工具的重要組成有了更深入的理解，從軟硬件開(kāi)發(fā)業(yè)界逐漸接受可靠性工具這一點(diǎn)就可以體現(xiàn)出來(lái)。
　　本書(shū)介紹了各種能解決軟件可靠性問(wèn)題的方法。理想情況下，形式化方法應(yīng)該用起來(lái)直觀，學(xué)起來(lái)簡(jiǎn)潔、快速，對(duì)開(kāi)發(fā)過(guò)程的影響微乎其微。本書(shū)對(duì)各種方法進(jìn)行了比較，揭示了它們各自的優(yōu)點(diǎn)和缺點(diǎn)，同時(shí)緊扣自動(dòng)機(jī)理論和邏輯這兩個(gè)主題。在盡可能減少背景知識(shí)介紹的前提下，本書(shū)向非專家讀者描述了多種技術(shù)，并且針對(duì)軟件工程領(lǐng)域的研究人員和專業(yè)人士介紹了一些高級(jí)技術(shù)。
　　本書(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)的研究方向，以及開(kāi)發(fā)新方法和改進(jìn)現(xiàn)有技術(shù)提出了有益的見(jiàn)解

作者簡(jiǎn)介

　　Doron A. Peled 以色列巴依蘭大學(xué)（BarIlan
University）計(jì)算機(jī)科學(xué)系教授。主要研究領(lǐng)域?yàn)椴l(fā)理論、形式化驗(yàn)證、形式化規(guī)約、編程語(yǔ)言語(yǔ)義、模型檢驗(yàn)、有限自動(dòng)機(jī)、軟件測(cè)試、時(shí)序邏輯等。著有多部書(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è)試等課程。

書(shū)籍目錄

出版者的話
中文版序　
譯者序
英文版序
前言
第1章　引言
　1.1　形式化方法
　1.2　開(kāi)發(fā)與學(xué)習(xí)形式化方法
　1.3　使用形式化方法
　1.4　應(yīng)用形式化方法
　1.5　本書(shū)概要
第2章　預(yù)備知識(shí)
　2.1　集合表示法
　2.2　字符串和語(yǔ)言
　2.3　圖
　2.4　計(jì)算復(fù)雜度和可計(jì)算性
　2.5　擴(kuò)展閱讀
第3章　邏輯和定理證明
　3.1　一階邏輯
　3.2　項(xiàng)
　　3.2.1　賦值和解釋
　　3.2.2　多個(gè)論域上的結(jié)構(gòu)
　3.3　一階公式
　3.4　命題邏輯
　3.5　證明一階邏輯公式
　　3.5.1　正向推理
　　3.5.2　反向推理
　3.6　證明系統(tǒng)的屬性
　　3.6.1　正確性
　　3.6.2　完備性
　　3.6.3　可判定性
　　3.6.4　結(jié)構(gòu)完備性
　3.7　證明命題邏輯屬性
　3.8　一個(gè)實(shí)用的證明系統(tǒng)
　3.9　證明示例
　3.10　機(jī)器輔助證明
　3.11　機(jī)械化定理證明器
　3.12　擴(kuò)展閱讀
第4章　軟件系統(tǒng)建模
　4.1　順序系統(tǒng)、并發(fā)系統(tǒng)及反應(yīng)式系統(tǒng)
　4.2　狀態(tài)
　4.3　狀態(tài)空間
　4.4　轉(zhuǎn)換系統(tǒng)
　4.5　轉(zhuǎn)換的粒度
　4.6　為程序建模的例子
　　4.6.1　整數(shù)除法
　　4.6.2　計(jì)算組合數(shù)
　　4.6.3　Eratosthenes篩法
　　4.6.4　互斥
　4.7　非確定性轉(zhuǎn)換
　4.8　將命題變量賦給狀態(tài)
　4.9　合并狀態(tài)空間
　4.10　線性視角
　4.11　分支視角
　4.12　公平性
　4.13　偏序視角
　　4.13.1　一個(gè)銀行系統(tǒng)的例子
　　4.13.2　線性化和全局狀態(tài)
　　4.13.3　一個(gè)簡(jiǎn)單的例子
　　4.13.4　偏序模型的應(yīng)用
　4.14　形式化建模
　4.15　一個(gè)項(xiàng)目的建模
　4.16　擴(kuò)展閱讀
第5章　形式化規(guī)約
　5.1　規(guī)約機(jī)制的屬性
　5.2　線性時(shí)序邏輯
　5.3　公理化LTL
　5.4　LTL規(guī)約示例
　　5.4.1　交通燈
　　5.4.2　順序程序的屬性
　　5.4.3　互斥
　　5.4.4　公平性條件
　5.5　無(wú)限字上的自動(dòng)機(jī)
　5.6　使用Büchi自動(dòng)機(jī)作為規(guī)約
　5.7　確定性Büchi自動(dòng)機(jī)
　5.8　其他規(guī)約機(jī)制
　5.9　復(fù)雜的規(guī)約
　5.10　規(guī)約的完整性
　5.11　擴(kuò)展閱讀
第6章　自動(dòng)驗(yàn)證
　6.1　狀態(tài)空間搜索
　6.2　狀態(tài)表示方法
　6.3　自動(dòng)機(jī)結(jié)構(gòu)體系
　6.4　合并Büchi自動(dòng)機(jī)
　　6.4.1　廣義Büchi自動(dòng)機(jī)
　　6.4.2　將廣義Büchi自動(dòng)機(jī)轉(zhuǎn)換為簡(jiǎn)單Büchi自動(dòng)機(jī)
　6.5　Büchi自動(dòng)機(jī)求補(bǔ)
　6.6　檢驗(yàn)空集
　6.7　模型檢驗(yàn)范例
　6.8　將LTL轉(zhuǎn)換為自動(dòng)機(jī)
　6.9　模型檢驗(yàn)的復(fù)雜度
　6.10　表示公平性
　6.11　檢驗(yàn)LTL規(guī)約
　6.12　安全屬性
　6.13　狀態(tài)空間爆炸問(wèn)題
　6.14　模型檢驗(yàn)的優(yōu)點(diǎn)
　6.15　模型檢驗(yàn)的缺點(diǎn)
　6.16　選擇自動(dòng)驗(yàn)證工具
　6.17　模型檢驗(yàn)項(xiàng)目
　6.18　模型檢驗(yàn)工具
　6.19　擴(kuò)展閱讀
第7章　演繹式軟件驗(yàn)證
　7.1　流程圖程序的驗(yàn)證
　7.2　含數(shù)組變量的驗(yàn)證
　　7.2.1　含數(shù)組變量賦值的問(wèn)題
　　7.2.2　修改證明系統(tǒng)
　7.3　完全正確性
　7.4　公理式程序驗(yàn)證
　　7.4.1　賦值公理
　　7.4.2　空語(yǔ)句公理
　　7.4.3　左強(qiáng)化規(guī)則
　　7.4.4　右弱化規(guī)則
　　7.4.5　順序組合規(guī)則
　　7.4.6　if-then-else規(guī)則
　　7.4.7　while規(guī)則
　　7.4.8　begin-end規(guī)則
　　7.4.9　示例：整數(shù)除法
　7.5　并發(fā)程序的驗(yàn)證
　7.6　演繹驗(yàn)證的優(yōu)點(diǎn)
　7.7　演繹驗(yàn)證的缺點(diǎn)
　7.8　證明系統(tǒng)的正確性和完備性
　7.9　組合性
　7.10　演繹驗(yàn)證工具
　7.11　擴(kuò)展閱讀
第8章　進(jìn)程代數(shù)與等價(jià)關(guān)系
　8.1　進(jìn)程代數(shù)
　8.2　通信系統(tǒng)的演算
　　8.2.1　動(dòng)作前綴
　　8.2.2　選擇
　　8.2.3　并發(fā)組合
　　8.2.4　限制符
　　8.2.5　重標(biāo)記
　　8.2.6　等式定義
　　8.2.7　agent 0
　　8.2.8　傳值agent
　8.3　示例：Dekker算法
　8.4　建模問(wèn)題
　8.5　agent之間的等價(jià)性
　　8.5.1　跡等價(jià)
　　8.5.2　失敗等價(jià)
　　8.5.3　模擬等價(jià)
　　8.5.4　互模擬和弱互模擬等價(jià)
　8.6　等價(jià)關(guān)系的層級(jí)
　8.7　用進(jìn)程代數(shù)研究并發(fā)
　8.8　計(jì)算互模擬等價(jià)
　8.9　LOTOS
　8.10　進(jìn)程代數(shù)工具
　8.11　擴(kuò)展閱讀
第9章　軟件測(cè)試
　9.1　審查和走查
　9.2　控制流覆蓋準(zhǔn)則
　　9.2.1　語(yǔ)句覆蓋
　　9.2.2　邊覆蓋
　　9.2.3　條件覆蓋
　　9.2.4　邊/條件覆蓋
　　9.2.5　條件組合覆蓋
　　9.2.6　路徑覆蓋
　　9.2.7　不同覆蓋準(zhǔn)則的比較
　　9.2.8　循環(huán)覆蓋
　9.3　數(shù)據(jù)流覆蓋準(zhǔn)則
　9.4　傳播路徑條件
　　9.4.1　示例：GCD程序
　　9.4.2　含有輸入語(yǔ)句的路徑
　9.5　等價(jià)類劃分
　9.6　待測(cè)代碼預(yù)處理
　9.7　檢查測(cè)試套件
　9.8　組合性
　9.9　黑盒測(cè)試
　9.10　概率測(cè)試
　9.11　測(cè)試的優(yōu)點(diǎn)
　9.12　測(cè)試的缺點(diǎn)
　9.13　測(cè)試工具
　9.14　擴(kuò)展閱讀
第10章　組合形式化方法
　10.1　抽象
　10.2　組合測(cè)試與模型檢驗(yàn)
　　10.2.1　直接檢驗(yàn)
　　10.2.2　黑盒系統(tǒng)
　　10.2.3　組合鎖自動(dòng)機(jī)
　　10.2.4　黑盒死鎖檢測(cè)
　　10.2.5　一致性測(cè)試
　　10.2.6　檢驗(yàn)重置的可靠性
　　10.2.7　黑盒檢驗(yàn)
　10.3　凈室方法
　　10.3.1　驗(yàn)證
　　10.3.2　證明審查
　　10.3.3　測(cè)試
　10.4　擴(kuò)展閱讀
第11章　可視化
　11.1　在形式化方法中運(yùn)用可視化
　11.2　消息序列圖
　11.3　可視化流程圖和狀態(tài)機(jī)
　11.4　層次狀態(tài)圖
　　11.4.1　層次化狀態(tài)
　　11.4.2　統(tǒng)一的出口和入口
　　11.4.3　并發(fā)
　　11.4.4　輸入和輸出
　11.5　程序文本的可視化
　11.6　Petri網(wǎng)
　11.7　可視化工具
　11.8　擴(kuò)展閱讀
結(jié)束語(yǔ)
參考文獻(xiàn)

章節(jié)摘錄

版權(quán)頁(yè)：插圖：早期的形式化方法是基于文本的，具體包括對(duì)系統(tǒng)的形式化表示、系統(tǒng)屬性的規(guī)約以及與工具、測(cè)試和驗(yàn)證結(jié)果的交互過(guò)程。近年來(lái)，研究人員和從業(yè)人員開(kāi)始意識(shí)到對(duì)軟件進(jìn)行可視化表示將會(huì)極大地提高軟件開(kāi)發(fā)效率。在許多情況下，人們通過(guò)對(duì)代碼的可視化表示的觀察，能夠得到一些新的信息，如不同的程序?qū)ο笠约八鼈冎g的關(guān)聯(lián)、控制流、通信模式等。這種直觀的理解是無(wú)法通過(guò)一行一行地閱讀代碼獲得的。使用可視化表示法的趨勢(shì)在軟件開(kāi)發(fā)方法學(xué)（如UML[46]）所使用的多種圖中都得到了最好的反映。這些不同種類的圖可以用于描述系統(tǒng)的體系結(jié)構(gòu)、系統(tǒng)中包含的不同進(jìn)程或?qū)ο?、進(jìn)程或?qū)ο蟮慕换?、進(jìn)程或?qū)ο蟮霓D(zhuǎn)換、典型和異常的執(zhí)行、系統(tǒng)模塊之間的關(guān)聯(lián)等等。本章將討論如何通過(guò)可視化表示來(lái)給形式化方法帶來(lái)益處。可視化系統(tǒng)所帶來(lái)的好處是我們可以把呆板的語(yǔ)法映射成圖形化對(duì)象之間的關(guān)系。例如，考慮一下，在描述自動(dòng)機(jī)時(shí)，使用狀態(tài)轉(zhuǎn)換圖或者使用包括初始及結(jié)束狀態(tài)的狀態(tài)轉(zhuǎn)換表，哪個(gè)更易于接受？由此可見(jiàn)，可視化的表示在演示動(dòng)態(tài)過(guò)程時(shí)有著獨(dú)特的優(yōu)勢(shì)。再如，在表示模型檢驗(yàn)中的某個(gè)反例時(shí)，一張標(biāo)記了執(zhí)行路徑的流程圖顯然要比只是簡(jiǎn)單地列出其所執(zhí)行過(guò)的代碼要更加直觀。11.1 在形式化方法中運(yùn)用可視化我們已經(jīng)見(jiàn)過(guò)了一些既可以用文本化也可以用圖形化描述的符號(hào)。其一是自動(dòng)機(jī)，它通過(guò)文本化或圖形化的方式來(lái)描述系統(tǒng)的組成成分。其二是流程圖，它使用圖的形式展示程序。這些示例展示了基于文字和基于圖形的兩種不同表示方法。這兩種表示方法之間的轉(zhuǎn)換都被形式化地定義過(guò)。形式化方法的工具通常允許用戶與圖形化的表示進(jìn)行交互。對(duì)象的添加、刪除、復(fù)制、大小調(diào)整、重定位、改變標(biāo)簽等都已經(jīng)基本上成為了圖形化表示方法中的標(biāo)準(zhǔn)操作。由于互聯(lián)網(wǎng)的廣泛使用，一些常見(jiàn)的選擇或者更新操作在屏幕上都是以同樣的感官展現(xiàn)。而這些帶給用戶的好處就是可以花費(fèi)更少的時(shí)間來(lái)熟悉一個(gè)新的系統(tǒng)。由于目前計(jì)算機(jī)對(duì)文本數(shù)據(jù)的處理仍優(yōu)于對(duì)圖形化數(shù)據(jù)的處理，所以基于可視化表示的工具通常需要在圖形化和文本化描述形式之間做轉(zhuǎn)換。基于文本的表示通常是存儲(chǔ)在文本文件里面的。當(dāng)工具需要使用這個(gè)表示的時(shí)候，需要先讀入這個(gè)文本文件，然后生成圖形化的表示，最終顯示出來(lái)。當(dāng)用戶通過(guò)和工具之間的交互改變了圖形化表示的時(shí)候，那么工具就要對(duì)應(yīng)地修改該文本表示。

編輯推薦

《軟件可靠性方法》編輯推薦：集中介紹目前常用的重要軟件可靠性方法，并將它們互作比較，這些方法包括：演繹驗(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)的研究方向，以及開(kāi)發(fā)新方法和改進(jìn)現(xiàn)有技術(shù)提出了有益的見(jiàn)解。

圖書(shū)封面

圖書(shū)標(biāo)簽Tags

無(wú)

評(píng)論、評(píng)分、閱讀與下載

---

    軟件可靠性方法 PDF格式下載

---