博士论文答辩-鲁棒灰箱演算的类型系统和代数性质研究

《博士论文答辩-鲁棒灰箱演算的类型系统和代数性质研究》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、鲁棒灰箱演算的类型系统和代数性质研究博士生：管旭东导师：尤晋元上海交大计算机科学与工程系分布计算技术中心2002.6博士论文答辩内容提要1.论文的背景2.灰箱演算，研究ROAM的原因3.演化类型系统4.ROAM的进程等价性5.演算的翻译及证明6.总结论文的创新处2002-62博士论文答辩-鲁棒灰箱演算论文的背景移动计算硬件移动、软件移动网络的广域化、全球化从技术到理论支持从程序设计理论（programminglanguagetheory）角度寻求支持并发(concurrency)、分布(distribution)、移动(mobility)概念的核心模

2、型（CCS,CSP,,,join,ambient,seal,...）目标：作为支持全球性移动计算编程语言的理论基础2002-63博士论文答辩-鲁棒灰箱演算相关研究领域本论文有关灰箱演算（ambientcalculus）的研究工作，属于：程序设计理论（并发、分布、移动）进程代数相关研究领域：OS(distributed/mobile):OSsupportforJavaandmobileagenttechnologyTCS:typetheoryandsemanticsSecurity-Wideareanetwork,softwaremobility2002-

3、64博士论文答辩-鲁棒灰箱演算灰箱演算的相关工作支持分布、移动的形式化模型，除了Ambient,还有：dist:Sekiguchi,et.al.,1997,U.TokyoD:Henessey,et.al.,1998,U.Sussex1l:Amadio,1997Distributed-:Sewell,1998,CambridgeD-join:Fournet,et.al.,1996,INRIASeal:Vitek,et.al,1999,U.Purdue...2002-65博士论文答辩-鲁棒灰箱演算内容提要1.论文的背景2.灰箱演算，研究ROAM的原因3.

4、演化类型系统4.ROAM的进程等价性5.pi演算的翻译及证明6.总结论文的创新处2002-66博士论文答辩-鲁棒灰箱演算MA在提出后迅速成为研究热点Cardelli&Gordon:“MobileAmbients”DigitalResearch=>MicrosoftResearch会议：FoSSaCS’98期刊：TheoreticalComputerScience,2000后续研究：Ambient有关的研究论文：50多篇FoSSaCS’98的引用数：200左右(http://citeseer.nj.nec.com/cardelli98mobile.html，2

5、002-05)(SCI引用数:50左右)欧盟：2002启动FET-GlobalComp.计划2002-67博士论文答辩-鲁棒灰箱演算MA用三个原语来描述移动计算cs[mail[outcs.inlib.Body]]

6、lib[openmail]libopenmailcsoutcs.inlib.Bodymail2002-68博士论文答辩-鲁棒灰箱演算out使一个灰箱移出其父灰箱libopenmailcsoutcs.inlib.Bodymaillibinlib.Bodymailopenmailcs2002-69博士论文答辩-鲁棒灰箱演算in使一个灰箱移进另一个同层灰

7、箱csinlib.BodymaillibopenmailBodymaillibopenmailcs2002-610博士论文答辩-鲁棒灰箱演算open用来打开一个灰箱BodymaillibopenmailcsBodylibcs2002-611博士论文答辩-鲁棒灰箱演算防火墙跨越体现了MA的安全性(page72)Agent=m[openk.k‘[Q]]Firewall=(w)(w[k[outw.inm.inw]

8、openm.openk‘.P])Agent

9、Firewall*(w)(w[P

10、Q])防火墙的一般形式：(w)(w[…])授信代理(Agent)跨

11、越防火墙(Firewall)：(mkk‘)(Agent

12、Firewall)(wmkk‘)(w[P

13、Q])2002-612博士论文答辩-鲁棒灰箱演算防火墙跨越前后的等价性推导(GC99)(mkk‘)(Agent

14、Firewall)(mkk‘w)(m[openk.k‘[Q]

15、k[inw]]

16、w[openm.openk‘.P])(mkk‘w)(w[m[k‘[Q]]

17、openm.openk‘.P])(mkk‘w)(w[k‘[Q]

18、openk‘.P])(mkk‘w)(w[Q

19、P])=(mkk‘)(m[openk.k‘[Q]]

20、(w)(w[k

21、[outw.inm.inw]

22、openm.openk