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

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

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