簡介
英文：Process Algebra
這些代數理論都使用通信，而不是共享存儲，作為進程之間相互作用的基本手段，表現出面向分散式系統的特徵。 在語法上，進程代數用一組運算元作為進程的構件。運算元的語義通常用結構化操作語義方法定義， 這樣進程就可看成是帶標號的變遷系統。進程代數 的一個顯著特徵是把並發性歸結為非確定性，將並 發執行的進程的行為看成是各單個進程的行為的所 有可能的交錯合成，即所謂交錯語義。 進程代數研究的核心問題是進程的等價性，即在什麼意義下兩個進程的行為相同?在進程代數領域使用的最為廣泛的等價關係有互模擬、測試等價、 失敗等價(參見通信順序進程)等。對這些語義等價 關係均建立了相應的公理系統。關於公理系統的研 究不僅加深了對語義理論的理解，而且使得有可能 對語義等價關係進行形式推理。 為了將進程代數的理論成果套用於解決實際問題，20世紀80年代後期出現了許多計算機支持工具。用這些工具可對進程的行為進行推理或模擬。
中國的研究者
林惠民林惠民院士主要從事軟體的基礎性研究。計算機是一種工具，大部分的人是在進行套用研究，即如何利用現有的理論和模型來開發出更有用的東西。而基礎性研究與套用研究不同，它不僅要關心怎么樣，還要知道為什麼這樣，要能夠提出新的模型和方法。計算機軟體科學的特點是基礎研究和套用研究是緊密結合的，而且時效性非常強，基礎研究的最新成果很快就會套用到工程中去。林惠民院士從事的一項工作是關於並發程式的形式語義學及形式化方法的研究。他和他的同事設計並實現了世界上第一個通用的進程代數驗證工具。進程代數的實際套用離不開計算機輔助工具的支持。八十年代後期，一批進程代數驗證工具應運而生（如CWB, PSF, LOTOSphere等），其共同局限性是每一工具只適用於某一特定的進程演算。這種局限性妨礙了驗證工具的推廣套用。如何克服這種局限性是當時國際進程代數界面臨的一個重大挑戰。這些驗證工具無法做到通用，根本原因在於缺乏既能描述不同進程演算的語義，又能為計算機所理解的通用語言。經過對不同演算的反覆比較，並考慮到在計算機上實現的可能性，他提煉出了一個元語言，用它可以描述各種進程演算的公理化語義，並且具有良好的可讀性。在此基礎上實現了通用的互動式進程代數驗證工具PAM，只要將這個元語言描述的進程演算定義輸入PAM，就得到該演算的證明器。PAM可同時接受多個不同的演算，對每個演算又可生成多個證明視窗。這是世界上第一個通用的進程代數證明工具。1993年他又利用當時剛剛取得的關於訊息傳送進程證明系統的理論結果，對PAM加以擴充，研製成迄今世界上唯一能對付訊息傳送進程的驗證工具VPAM。PAM和VPAM都是通過ftp在Internet上公開發行的，其用戶遍布各大洲，包括美國、加拿大、英、法、德、意、荷蘭、丹麥、瑞典、斯洛伐克、巴西、印度、紐西蘭、南非等十幾個國家，其中既有來自大學的，也有來自菲利普、惠普和貝爾等著名公司實驗室的。
