軟件可靠性方法

內容概要

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

作者簡介

　　Doron A. Peled 以色列巴依蘭大學（BarIlan
University）計算機科學系教授。主要研究領域為并發(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　整數除法
　　4.6.2　計算組合數
　　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　含數組變量的驗證
　　7.2.1　含數組變量賦值的問題
　　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　示例：整數除法
　7.5　并發(fā)程序的驗證
　7.6　演繹驗證的優(yōu)點
　7.7　演繹驗證的缺點
　7.8　證明系統(tǒng)的正確性和完備性
　7.9　組合性
　7.10　演繹驗證工具
　7.11　擴展閱讀
第8章　進程代數與等價關系
　8.1　進程代數
　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　用進程代數研究并發(fā)
　8.8　計算互模擬等價
　8.9　LOTOS
　8.10　進程代數工具
　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　數據流覆蓋準則
　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　擴展閱讀
結束語
參考文獻

章節(jié)摘錄

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

編輯推薦

《軟件可靠性方法》編輯推薦：集中介紹目前常用的重要軟件可靠性方法，并將它們互作比較，這些方法包括：演繹驗證、自動驗證、測試和進程代數，為具體項目的軟件選擇過程提供有用信息，提供了大量的練習、項目和連續(xù)性的實例，方便讀者學習形式化方法并能夠親手使用這些工具介紹了支持形式化方法的數學原理，對于該領域未來的研究方向，以及開發(fā)新方法和改進現有技術提出了有益的見解。

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

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

---