反應(yīng)系統(tǒng)的建模規(guī)約與驗(yàn)證

Ｌ．埃斯托等

計(jì)算機(jī)科學(xué)建造人工制品，這些人工制品應(yīng)為用戶提供某些明確的服務(wù)。它們正確地完成所擔(dān)負(fù)目的的行為規(guī)約是至關(guān)重要的。確定計(jì)算系統(tǒng)是否確實(shí)提供了由它的規(guī)約所描述的行為問題叫做正確性問題，它是計(jì)算機(jī)科學(xué)中最基本的問題。研究描述計(jì)算機(jī)模型及它們的規(guī)約，以及根據(jù)它們的規(guī)約建立系統(tǒng)正確性的方法(有可能是自動(dòng)的)，叫做算法驗(yàn)證。

一個(gè)反應(yīng)系統(tǒng)是由計(jì)算組件網(wǎng)絡(luò)組成的，并且通過在它們自身及所處環(huán)境的交互使用來達(dá)到它們的目的。因此甚至相對(duì)小的系統(tǒng)也有可能展現(xiàn)意想不到的復(fù)雜行為，而且由于反應(yīng)系統(tǒng)經(jīng)常被用于安全關(guān)鍵系統(tǒng)，因此對(duì)基于數(shù)學(xué)的形式方法學(xué)需求是不斷地增強(qiáng)。

本書向研究生提供了更為全面的介紹，描述了各種各樣的方法，各種方法的優(yōu)缺點(diǎn)以及何時(shí)使用它們最佳。

本書介紹了米爾納的通訊系統(tǒng)演算(ccs)和它的操作語(yǔ)義學(xué)，連同建立在互模擬技術(shù)基礎(chǔ)上的等價(jià)概念和亨尼斯一米爾納邏輯(HML)的遞歸擴(kuò)展。本書的第二部分中所介紹的理論被拓展到考慮時(shí)間問題。

本書共有13章，分成二大部分。第一部分反應(yīng)系統(tǒng)的經(jīng)典理論，含第1～7章。1.緒論；2.CCS語(yǔ)言；3.行為等價(jià)；4.固定點(diǎn)理論與互模擬等價(jià)；5.HML；6.HML與遞歸；7.建模互斥法算法。第二部分實(shí)時(shí)系統(tǒng)理論，含第8～13章。8.入門；9.CCS與時(shí)間延遲；10.計(jì)時(shí)自動(dòng)機(jī)；11.計(jì)時(shí)行為等價(jià)；12.HML與時(shí)間；13.建模與費(fèi)希爾算法分析。最后是附錄A對(duì)學(xué)生項(xiàng)目的建議。本書的內(nèi)容是建立在作者過去6年左右在丹麥Aalborg大學(xué)和冰島的雷克雅未克大學(xué)所開設(shè)的課程之上的，它向?qū)W生提供了一個(gè)對(duì)該領(lǐng)域的廣泛介紹。

本書引導(dǎo)讀者理解并掌握過程代數(shù)，是一本出色的大學(xué)高年級(jí)教課書。