軟件可靠性方法

定　價：￥45.00

作　者：	（以）佩萊得著，王林章等譯
出版社：	機械工業(yè)出版社
叢編項：
標　簽：	軟件工程/開發(fā)項目管理

購買這本書可以去

ISBN：	9787111365532	出版時間：	2012-03-01	包裝：	平裝
開本：	大32開	頁數(shù)：	196	字數(shù)：

內容簡介

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

作者簡介

　　Doron A. Peled 以色列巴依蘭大學（BarIlanUniversity）計算機科學系教授。主要研究領域為并發(fā)理論、形式化驗證、形式化規(guī)約、編程語言語義、模型檢驗、有限自動機、軟件測試、時序邏輯等。著有多部書籍和論文。王林章南京大學計算機科學與技術系副教授、碩士生導師，南京大學計算機軟件新技術國家重點實驗室主任助理。主要研究方向為軟件工程、新型軟件測試方法、模型驅動軟件測試與驗證、自動化軟件測試工具。目前面向本科生、研究生講授軟件工程、軟件體系結構、軟件測試等課程。

圖書目錄

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