掃一掃
關注中圖網(wǎng)
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰(zhàn)行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優(yōu)實踐之路
-
>
第一行代碼Android
-
>
JAVA持續(xù)交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
形式化方法導論(第2版) 版權信息
- ISBN：9787302626602
- 條形碼：9787302626602 ; 978-7-302-62660-2
- 裝幀：一般膠版紙
- 冊數(shù)：暫無
- 重量：暫無
- 所屬分類：>
形式化方法導論(第2版) 本書特色
形式化方法是軟件工程專業(yè)的核心課程，但相關教材稀缺，本書彌補了這一空白，內(nèi)容全面，適合教學。 全面講解形式化方法，評為江蘇省高等學校重點教材
形式化方法導論(第2版) 內(nèi)容簡介
形式化方法是指有嚴格數(shù)學基礎的軟件和系統(tǒng)開發(fā)方法，支持軟件與系統(tǒng)的規(guī)約、設計、驗證與演化等活動。隨著軟件可信需求的不斷增長，形式化方法的重要性和關注度日益提高。 本書共12章，第1章概述形式化方法，第2章介紹形式化方法發(fā)展早期的經(jīng)典內(nèi)容，其余部分共分3篇： 上篇（第3～5章）為系統(tǒng)建模篇，著重介紹遷移系統(tǒng)、有窮自動機、Petri網(wǎng)等基本計算模型； 中篇（第6和第7章）為形式規(guī)約篇，著重討論時序邏輯及其在并發(fā)系統(tǒng)屬性描述的應用； 下篇（第8～12章）為形式驗證篇，著重介紹定理證明方法和并發(fā)、實時及混成系統(tǒng)的各種模型檢測方法及相關驗證工具。全書提供了大量應用實例，每章后均附有習題。 本書適合作為高等院校計算機、軟件工程、人工智能、網(wǎng)絡工程、信息安全、自動化等專業(yè)高年級本科生、研究生的教材，同時可供相關領域的研究人員和技術開發(fā)人員參考。
形式化方法導論(第2版) 目錄
目錄
第1章緒論
1.1形式化方法的發(fā)展歷程
1.2形式化方法的基本內(nèi)容
1.2.1系統(tǒng)建模
1.2.2形式規(guī)約
1.2.3形式驗證
1.3本章小結
習題1
第2章程序正確性證明
2.1Floyd前后斷言法
2.1.1基本概念
2.1.2證明方法
2.1.3應用舉例
2.2Hoare公理化方法
2.2.1基本概念
2.2.2證明方法
2.2.3應用舉例
2.3Dijkstra*弱前置條件方法
2.3.1基本概念
2.3.2證明方法
2.3.3應用舉例
2.4本章小結
習題2
上篇系 統(tǒng) 建 模
第3章遷移系統(tǒng)
3.1基本概念
3.1.1形式定義
3.1.2遷移圖
3.1.3計算
3.2應用舉例
3.2.1時序電路
3.2.2數(shù)據(jù)依賴系統(tǒng)
3.2.3并發(fā)和交錯
3.3本章小結
習題3
第4章自動機
4.1有窮自動機
4.1.1有窮狀態(tài)系統(tǒng)
4.1.2形式定義
4.1.3判定算法
4.2Büchi自動機
4.2.1ω有窮自動機簡介
4.2.2Büchi自動機
4.2.3應用舉例
4.3本章小結
習題4
第5章Petri網(wǎng)
5.1庫所/變遷Petri網(wǎng)
5.1.1基本概念
5.1.2基本性質
5.1.3分析方法
5.1.4應用舉例
5.2謂詞/變遷Petri網(wǎng)
5.2.1基本概念
5.2.2應用舉例
5.3著色Petri網(wǎng)
5.3.1基本概念
5.3.2應用舉例
5.4本章小結
習題5
中篇形 式 規(guī) 約
第6章時序邏輯
6.1線性時序邏輯
6.1.1LTL語法
6.1.2LTL語義
6.1.3應用舉例
6.2分支時序邏輯
6.2.1CTL語法
6.2.2CTL語義
6.2.3應用舉例
6.3區(qū)間時序邏輯簡介
6.4本章小結
習題6
第7章并發(fā)系統(tǒng)屬性
7.1基本概念
7.2安全性
7.2.1形式定義
7.2.2形式描述
7.2.3應用舉例
7.3活性
7.3.1形式定義
7.3.2形式描述
7.3.3應用舉例
7.4本章小結
習題7
下篇形 式 驗 證
第8章定理證明
8.1時序邏輯演繹驗證方法
8.1.1PLTL邏輯系統(tǒng)
8.1.2MannaPnueli演繹規(guī)則方法
8.1.3驗證工具STeP及應用
8.2自動定理證明方法
8.2.1SAT求解算法
8.2.2SMT求解技術
8.2.3ATP方法小結
8.3交互式定理證明方法
8.3.1主要證明輔助工具簡介
8.3.2應用舉例
8.3.3ITP方法小結
8.4本章小結
習題8
第9章模型檢測
9.1基本概念
9.2模型檢測算法
9.2.1CTL模型檢測算法
9.2.2LTL模型檢測算法
9.3模型檢測工具及應用
9.3.1驗證工具SPIN
9.3.2應用舉例
9.4本章小結
習題9
第10章符號模型檢測
10.1二叉判定圖
10.1.1基本概念
10.1.2約簡方法
10.1.3Apply操作及應用
10.2CTL符號模型檢測
10.2.1基本方法
10.2.2驗證工具SMV
10.2.3應用舉例
10.3LTL符號模型檢測簡介
10.4本章小結
習題10
第11章概率模型檢測
11.1概率模型
11.1.1離散時間馬爾可夫鏈
11.1.2馬爾可夫決策過程
11.1.3連續(xù)時間馬爾可夫鏈
11.2概率時序邏輯
11.2.1概率計算樹邏輯
11.2.2連續(xù)隨機邏輯
11.3概率模型檢測工具及應用
11.3.1驗證工具PRISM
11.3.2應用舉例
11.4本章小結
習題11
第12章實時與混成系統(tǒng)驗證
12.1時間自動機
12.1.1語法
12.1.2語義
12.2實時邏輯
12.2.1時間計算樹邏輯
12.2.2度量區(qū)間時序邏輯
12.3實時系統(tǒng)模型檢測
12.3.1基本方法
12.3.2驗證工具UPPAAL
12.3.3應用舉例
12.4混成系統(tǒng)驗證簡介
12.4.1混成自動機
12.4.2微分動態(tài)邏輯
12.4.3混成系統(tǒng)模型檢測
12.5本章小結
習題12
參考文獻
展開全部
書友推薦
- >
人文閱讀與收藏·良友文學叢書:一天的工作
- >
回憶愛瑪儂
- >
李白與唐代文化
- >
羅庸西南聯(lián)大授課錄
- >
朝聞道
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語)
- >
大紅狗在馬戲團-大紅狗克里弗-助人
- >
詩經(jīng)-先民的歌唱
本類暢銷
