魯棒灰箱演算的類型系統(tǒng)和代數性質研究.pdf

1、灰箱演算是一種用于描述移動系統(tǒng)及其交互的形式化方法.該文以灰箱演算的一個變體--魯棒灰箱演算（ROAM）作為研究對象,從操作語義、類型系統(tǒng)、進程等價性和表達能力等方面對其進行了研究.該文的主要貢獻在于.（一）對利用協(xié)動作參數加強灰箱演算安全性這一命題進行了研究,提出了灰箱演算的變體ROAM.通過利用協(xié)動作參數加強交互雙方的彼此控制,ROAM在安全控制方面比起SA來有一定優(yōu)勢.同時,對協(xié)動作參數進行控制后,ROAM并沒有喪失SA所具有的表

2、達能力.（二）針對灰箱演算中存在的類型演化問題給出了支持移動性和線程數的演化類型系統(tǒng)ETS-MT.ETS-MT通過區(qū)分進程的當前類型和未來類型,可以精確地刻劃進程的移動性和線程數,并支持子類型關系.考慮到類型系統(tǒng)中所刻劃屬性的增減,ETS-MT在設計時還專門引入準類型集合的概念,刻劃不同的類型屬性,可以有不同的準類型集合.（三）將前人對灰箱演算語義、等價性、表達能力等方面的研究成果進行了貫穿和融合,集中體現在兩方面.首先,有別于Levi