系統(tǒng)工程Petri網(wǎng)

內(nèi)容概要

本書是一本關(guān)于Petri網(wǎng)的建模、驗證與應(yīng)用的優(yōu)秀的教學(xué)與研究參考書。全書分為5個部分共27章，首先講解了Petri網(wǎng)的基本概念，通過實例介紹了常量弧網(wǎng)、庫所/變遷網(wǎng)和有色網(wǎng)的基本定義。作者接著討論了如何應(yīng)用Petri網(wǎng)來構(gòu)造系統(tǒng)，并給出了各種建模的方法。書中介紹了對Petri網(wǎng)模型進(jìn)行驗證的主要方法，其中包括基于狀態(tài)空間的方法和模型檢驗、結(jié)構(gòu)方法以及使用演繹和進(jìn)程代數(shù)的一些高級方法；講解了Petri網(wǎng)的確認(rèn)和執(zhí)行，其中不僅涉及到軟件生命周期的相關(guān)內(nèi)容，而且詳細(xì)介紹了在復(fù)雜系統(tǒng)的開發(fā)過程中如何使用Petri網(wǎng)進(jìn)行建模和分析。最后，作者對Petri網(wǎng)的三個不同應(yīng)用領(lǐng)域（柔性制造系統(tǒng)、工作流管理系統(tǒng)和電信系統(tǒng)）進(jìn)行了深入的研究。本書的內(nèi)容全面，結(jié)構(gòu)清晰，并通過大量實例講解了各種概念、方法與應(yīng)用。   本書可以作為計算機(jī)相關(guān)專業(yè)本科生和研究生的教材或參考書，也可作為從事軟件系統(tǒng)研究的人員的寶貴參考資料。

作者簡介

袁崇義，北京大學(xué)計算機(jī)系教授、博士生導(dǎo)師，中國計算機(jī)學(xué)會理事，Petri網(wǎng)專業(yè)委員會主任，主要出版著作有《Petri網(wǎng)原理》。袁崇義教授的研究方向有：Petri網(wǎng)的基本理論，包括同步論和網(wǎng)邏輯；Petri網(wǎng)應(yīng)用，特別是在并行計算方面的應(yīng)用和工作流方面的應(yīng)用；并行計算的基本理

書籍目錄

第一部分 Petri網(wǎng)——基本概念  第1章 引言  第2章 Petri網(wǎng)的實質(zhì)特征    2.1 局部確定性和并發(fā)    2.2 圖形表示和代數(shù)表示    2.3 并發(fā)、沖突和混惑    2.4 細(xì)化和組合    2.5 網(wǎng)射  第3章 直觀模型    3.1 常量弧網(wǎng)    3.2 庫所／變遷網(wǎng)    3.3 有色網(wǎng)    3.4 折疊   第4章 基本定義    4.1 庫所／變遷網(wǎng)的形式化定義    4.2 常量弧網(wǎng)的形式化定義    4.3 有色網(wǎng)的形式化定義  第5章 性質(zhì)    5.1 基本性質(zhì)    5.2 分析方法介紹  第6章 本書總覽第二部分 建 模  第7章 引言  第8章 實例解說建模和分析技術(shù)    8.1 網(wǎng)、優(yōu)化和抽象    8.2 庫所／變遷網(wǎng)和資源管理    8.3 有色網(wǎng)、抽象和展開  第9章 技術(shù)    9.1 構(gòu)建塊    9.2 結(jié)合網(wǎng)    9.3 高級網(wǎng)    9.4 分解網(wǎng)    9.5 小結(jié)  第10章 方法    10.1 面向狀態(tài)建模    10.2 面向事件的建模    10.3 面向?qū)ο蠼? 第11章實例研究    11.1 面向狀態(tài)的方法    11.2 面向事件的方法    11.3 面向?qū)ο蠓椒? 第12章 小結(jié)第三部分 驗 證  第13章 引言：驗證所涉及的問題    13.1 網(wǎng)的分類    13.2 性質(zhì)    13.3 方法分類    13.4 驗證過程    13.5 概述  第14章 基于狀態(tài)空間的方法與模型檢驗    14.1 性質(zhì)、時態(tài)邏輯及公平性    14.2 On—the—nv方法    14.3 基于偏序的方法    14.4 符號化和參數(shù)化方法    14.5 實現(xiàn)問題    14.6 綜合及一般性總結(jié)評注  第15章 結(jié)構(gòu)方法    15.1 網(wǎng)系統(tǒng)歸約    15.2 線性代數(shù)技術(shù)    15.3 虹吸和陷阱    15.4 網(wǎng)子類的分析    15.5 不變量和有色Petri網(wǎng)的歸約  第16章 演繹與基于進(jìn)程代數(shù)的方法    16.1 代數(shù)網(wǎng)的重寫語義    16.2 斷言推理    16.3 授權(quán)邏輯    16.4 線性邏輯和Petri網(wǎng)    16.5 利用進(jìn)程代數(shù)驗證Petri網(wǎng)模型  第17章 小結(jié)第四部分 確認(rèn)和執(zhí)行  第18章 引言  第19章 系統(tǒng)工程和確認(rèn)    19.1 軟件生命周期和確認(rèn)    19.2 確認(rèn)    19.3 一種方法——原型建立    19.4 工具  第20章 網(wǎng)的運(yùn)行    20.1 集中控制    20.2 將控制分發(fā)給庫所    20.3 將控制分發(fā)給邊    20.4 多線程和同步    20.5 異步    20.6 小結(jié)  第21章 代碼生成    21.1 對于代碼生成的Petri網(wǎng)方法    21.2 Petri網(wǎng)的劃分算法    21.3 Petri網(wǎng)中代碼生成的一些方面    21.4 高級網(wǎng)中的代碼生成    21.5 小結(jié)  第22章 小結(jié)第五部分 應(yīng)用領(lǐng)域  第23章 引言    23.1 工作中應(yīng)用Petri網(wǎng)    23.2 應(yīng)用領(lǐng)域  第24章 柔性制造系統(tǒng)    24.1 領(lǐng)域概覽    24.2 在FMS中使用Petri網(wǎng)    24.3 設(shè)計方法    24.4 小結(jié)  第25章 工作流系統(tǒng)    25.1 領(lǐng)域概述    25.2 動機(jī)    25.3 設(shè)計方法學(xué)    25.4 工作流分析    25.5 實例學(xué)習(xí)：Sagitta-2000案例    25.6 小結(jié)  第26章 電信系統(tǒng)    26.1 領(lǐng)域概述    26.2 動機(jī)    26.3 設(shè)計方法學(xué)    26.4 分析    26.5 小結(jié)  第27章 小結(jié)    27.1 公共建模問題    27.2 共享的分析結(jié)果術(shù)語表參考文獻(xiàn)

編輯推薦

　　越來越大、越來越復(fù)雜的系統(tǒng)，使得應(yīng)用在硬件和軟件的規(guī)范與驗證中的形式化方法越來越重要。本書旨在通過Petri網(wǎng)的形式化過程來闡述形式化方法中的相關(guān)進(jìn)展。書中采用了許多實例，它們來源于不同的應(yīng)用領(lǐng)域，例如柔性制造系統(tǒng)、工作流管理系統(tǒng)和電信系統(tǒng)。本書的內(nèi)容涵蓋了一個系統(tǒng)在設(shè)計和實現(xiàn)的整個生命周期中的幾個主要階段，即規(guī)范、用于證明的模型驗證技術(shù)、性質(zhì)分析、代碼生成和模型的執(zhí)行。書中對這些技術(shù)及其支持工具進(jìn)行了詳細(xì)的討論，并且分析了在實際應(yīng)用中可能遇到的問題。

圖書封面

圖書標(biāo)簽Tags

無

評論、評分、閱讀與下載

---

    系統(tǒng)工程Petri網(wǎng) PDF格式下載

---