前 言

公允地說(shuō), 在這個(gè)數(shù)字時(shí)代, 正確的信息處理系統(tǒng)比黃金更可貴.

——摘自 H. Barendregt 的“The Quest for Correctness”,

發(fā)表于Images of SMC Research 1996，第39~58頁(yè).

本書(shū)講述模型檢驗(yàn), 它是一種評(píng)估信息及通信系統(tǒng)的功能性質(zhì)的很好的形式化技術(shù). 模型檢驗(yàn)需要考慮系統(tǒng)的一個(gè)模型及期望的性質(zhì), 并系統(tǒng)地檢驗(yàn)給定模型是否滿(mǎn)足此性質(zhì). 可以驗(yàn)證的典型性質(zhì)是無(wú)死鎖、不變性以及請(qǐng)求與響應(yīng)性質(zhì). 模型檢驗(yàn)是驗(yàn)證模型不含錯(cuò)誤\ (即不違反性質(zhì)) 的自動(dòng)技術(shù), 也可看作智能、高效的調(diào)試技術(shù). 它是一種通用方法, 已被用于硬件驗(yàn)證及軟件工程等領(lǐng)域. 模型檢驗(yàn)技術(shù)在二十多年前只能用于簡(jiǎn)單的例子. 但隨著基礎(chǔ)算法及數(shù)據(jù)結(jié)構(gòu)的不斷改進(jìn)及硬件水平的進(jìn)步, 它現(xiàn)在已經(jīng)可以用于實(shí)際設(shè)計(jì)中. 客觀地講, 過(guò)去二十多年中, 模型檢驗(yàn)已經(jīng)發(fā)展為成熟的并被大量使用的驗(yàn)證和調(diào)試技術(shù).

目的與范圍

本書(shū)將從基本原理開(kāi)始介紹模型檢驗(yàn). 本書(shū)可作為本科生和研究生的教材, 也可作為計(jì)算機(jī)科學(xué)及相關(guān)領(lǐng)域研究者的入門(mén)讀物. 本書(shū)用大量的例子向讀者介紹相關(guān)的材料, 許多例子會(huì)貫穿多個(gè)章節(jié). 本書(shū)提供完整的基本結(jié)論及其詳細(xì)證明. 每章后面都有總結(jié)、文獻(xiàn)說(shuō)明及關(guān)于一系列理論與實(shí)踐(即實(shí)際模型檢驗(yàn)器的實(shí)驗(yàn)) 的習(xí)題.

基礎(chǔ)知識(shí)

模型檢驗(yàn)中的概念起源于數(shù)學(xué), 例如命題邏輯、自動(dòng)機(jī)理論與形式語(yǔ)言、 數(shù)據(jù)結(jié)構(gòu)以及圖論算法. 盡管本書(shū)附錄概括了這些內(nèi)容的要點(diǎn), 但是讀者還是要在學(xué)習(xí)本書(shū)正文前熟悉這些基本知識(shí). 當(dāng)考慮許多模型檢驗(yàn)算法的理論復(fù)雜度時(shí), 還需要 復(fù)雜度理論的相關(guān)知識(shí).

內(nèi)容

本書(shū)分為10章. 第1章概述模型檢驗(yàn)及其特征. 第2章給出作為軟件和硬件系統(tǒng)模型的遷移系統(tǒng). 第3章介紹線性時(shí)間性質(zhì)的安全性質(zhì)與活性性質(zhì)的分類(lèi), 并闡述公平性的概念. 檢驗(yàn)(正則) 安全性質(zhì)和?正則性質(zhì)的基于自動(dòng)機(jī)的算法在第4章中論述. 第5章闡述線性時(shí)序邏輯 (LTL), 并指出第4章的算法如何用于LTL 模型檢驗(yàn). 第6章論述分支時(shí)序邏輯——計(jì)算樹(shù)邏輯(CTL), 并將其與LTL進(jìn)行比較, 然后指出如何明確地或符號(hào)化地進(jìn)行CTL 模型檢驗(yàn). 第7章論述基于跡、互模擬及模擬關(guān)系的抽象. 第8章講述LTL 和CTL 的偏序約簡(jiǎn). 第9章著重介紹實(shí)時(shí)時(shí)間性質(zhì)與時(shí)控自動(dòng)機(jī). 最后, 本書(shū)以概率模型的驗(yàn)證結(jié)束. 附錄概括了命題邏輯、圖論、形式語(yǔ)言以及復(fù)雜度理論的基礎(chǔ)知識(shí).

如何使用此書(shū)

第1章至第6章可作為一學(xué)期(每周兩次課) 的模型檢驗(yàn)入門(mén)課程的內(nèi)容. 在后續(xù)一學(xué)期的課程中, 可在稍微復(fù)習(xí)LTL 和CTL 模型檢驗(yàn)后學(xué)完第7章至第10章的內(nèi)容.

致謝

本書(shū)的寫(xiě)作與擴(kuò)充花費(fèi)了5年的時(shí)間. 以下同仁通過(guò)使用本書(shū)的早期版本給予我們支持: Luca Aceto (丹麥奧爾堡大學(xué), 冰島雷克雅未克大學(xué)), Henrik Reif Andersen (丹麥哥本哈根大學(xué)), Dragan Boshnacki (荷蘭艾因霍溫大學(xué)), Franck van Breughel (加拿大渥太華大學(xué)), Josée Desharnais (加拿大魁北克大學(xué)), Susanna Donatelli (意大利都靈大學(xué)), Stefania Gnesi (意大利比薩大學(xué)), Michael R. Hansen (丹麥技術(shù)大學(xué)), Holger Hermanns (德國(guó)薩爾布呂肯大學(xué)), Yakov Kesselman (美國(guó)芝加哥大學(xué)), Martin Lange (丹麥奧爾胡斯大學(xué)), Kim G. Larsen (丹麥奧爾堡大學(xué)), Mieke Massink (意大利比薩大學(xué)), Mogens Nielsen (丹麥奧爾胡斯大學(xué)), Albert Nymeyer (澳大利亞悉尼大學(xué)), Andreas Podelski (德國(guó)弗萊堡大學(xué)), Theo C. Ruys (荷蘭特文特大學(xué)), Thomas Schwentick (德國(guó)多特蒙德大學(xué)), Wolfgang Thomas (德國(guó)亞琛大學(xué)), Julie Vachon (加拿大蒙特利爾大學(xué)), 以及Glynn Winskel (英國(guó)劍橋大學(xué)). 他們中的許多人都給了非常有益的反饋, 使我們得以完善本書(shū).

Henrik Bohnenkamp、Tobias Blechmann、Frank Ciesinski、Marcus Gr?sser、Tingting Han、 Joachim Klein、Sascha Klüppelholz、Miriam Nasfi、Martin Neuh?usser 和Ivan S. Zapreev 給我們提供了許多詳細(xì)的意見(jiàn)和一些習(xí)題. Yen Cao 繪制了部分圖形, Ulrich Schmidt-G?rtz 提供了參考文獻(xiàn)方面的幫助. 在此 誠(chéng)摯地感謝他們.

許多人對(duì)本書(shū)提出過(guò)改進(jìn)建議, 指出過(guò)疏漏. 感謝提出寶貴意見(jiàn)的每一位同仁.

最后, 感謝我們?cè)趤嗚�、波恩、德累斯頓與恩斯赫德的所有學(xué)生的反饋和意見(jiàn).

Christel Baier

Joost-Pieter Katoen