前 言

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

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

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

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

目的與范圍

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

基礎(chǔ)知識

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

內(nèi)容

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

如何使用此書

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

致謝

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

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

許多人對本書提出過改進建議, 指出過疏漏. 感謝提出寶貴意見的每一位同仁.

最后, 感謝我們在亞琛、波恩、德累斯頓與恩斯赫德的所有學生的反饋和意見.

Christel Baier

Joost-Pieter Katoen