PAGEPAGE4畢業(yè)設(shè)計(jì)（論文）開題報(bào)告題目進(jìn)程交互消息可見性研究專業(yè)信息與計(jì)算科學(xué)姓名班級(jí)學(xué)號(hào)指導(dǎo)教師提交時(shí)間一、綜述本課題的研究動(dòng)態(tài)，說(shuō)明選題的依據(jù)和意義1、本課題研究動(dòng)態(tài)進(jìn)程代數(shù)是關(guān)于通信并發(fā)系統(tǒng)的代數(shù)理論的統(tǒng)稱。20世紀(jì)70年代后期，英國(guó)學(xué)者RMnner和C.A.R，分別提出了通信系統(tǒng)演算和通信順序進(jìn)程，開創(chuàng)了用代數(shù)方法研究通信并發(fā)系統(tǒng)的先河。此后這一研究方向興盛不衰，出現(xiàn)了眾多類似而又相互區(qū)別的演算系統(tǒng)，如ACP(提出者J.A.Ber郎tra和J.W.K10p)，ATp(提出者M(jìn).H即n櫻y)，Meije(提出者G.Eudol，R.desi~)，LOTC6等，統(tǒng)稱為進(jìn)程代數(shù)。這些代數(shù)理論都使用通信，而不是共享存儲(chǔ)，作為進(jìn)程之間相互作用的基本手段，表現(xiàn)出面向分布式系統(tǒng)的特征。在語(yǔ)法上，進(jìn)程代數(shù)用一組算子作為進(jìn)程的構(gòu)件。算子的語(yǔ)義通常用結(jié)構(gòu)化操作語(yǔ)義方法定義，這樣進(jìn)程就可看成是帶標(biāo)號(hào)的變遷系統(tǒng)。進(jìn)程代數(shù)的一個(gè)顯著特征是把并發(fā)性歸結(jié)為非確定性，將并發(fā)執(zhí)行的進(jìn)程的行為看成是各單個(gè)進(jìn)程的行為的所有可能的交錯(cuò)合成，即所謂交錯(cuò)語(yǔ)義。林惠民院士從事的一項(xiàng)工作是關(guān)于并發(fā)程序的形式語(yǔ)義學(xué)及形式化方法的研究。他和他的同事設(shè)計(jì)并實(shí)現(xiàn)了世界上第一個(gè)通用的進(jìn)程代數(shù)驗(yàn)證工具。進(jìn)程代數(shù)的實(shí)際應(yīng)用離不開計(jì)算機(jī)輔助工具的支持。八十年代后期，一批進(jìn)程代數(shù)驗(yàn)證工具應(yīng)運(yùn)而生（如CWB,PSF,LOTOSphere等），其共同局限性是每一工具只適用于某一特定的進(jìn)程演算。這種局限性妨礙了驗(yàn)證工具的推廣應(yīng)用。如何克服這種局限性是當(dāng)時(shí)國(guó)際進(jìn)程代數(shù)界面臨的一個(gè)重大挑戰(zhàn)。這些驗(yàn)證工具無(wú)法做到通用，根本原因在于缺乏既能描述不同進(jìn)程演算的語(yǔ)義，又能為計(jì)算機(jī)所理解的通用語(yǔ)言。經(jīng)過(guò)對(duì)不同演算的反復(fù)比較，并考慮到在計(jì)算機(jī)上實(shí)現(xiàn)的可能性，他提煉出了一個(gè)元語(yǔ)言，用它可以描述各種進(jìn)程演算的公理化語(yǔ)義，并且具有良好的可讀性。在此基礎(chǔ)上實(shí)現(xiàn)了通用的交互式進(jìn)程代數(shù)驗(yàn)證工具PAM，只要將這個(gè)元語(yǔ)言描述的進(jìn)程演算定義輸入PAM，就得到該演算的證明器。PAM可同時(shí)接受多個(gè)不同的演算，對(duì)每個(gè)演算又可生成多個(gè)證明窗口。這是世界上第一個(gè)通用的進(jìn)程代數(shù)證明工具。1993年他又利用當(dāng)時(shí)剛剛?cè)〉玫年P(guān)于消息傳送進(jìn)程證明系統(tǒng)的理論結(jié)果，對(duì)PAM加以擴(kuò)充，研制成迄今世界上唯一能對(duì)付進(jìn)程消息傳送的驗(yàn)證工具VPAM。2、選題的依據(jù)和意義進(jìn)程指的是系統(tǒng)的行為，系統(tǒng)是展示行為的系統(tǒng)，特別是一個(gè)軟件執(zhí)行、一個(gè)機(jī)器動(dòng)作，甚至一個(gè)人的動(dòng)作更是如此。作為控制并發(fā)系統(tǒng)復(fù)雜度和保證并發(fā)系統(tǒng)設(shè)計(jì)正確性和服務(wù)質(zhì)量的一種有效的手段，形式化方法的研究經(jīng)過(guò)幾十年努力，取得很大成績(jī)，相應(yīng)技術(shù)已經(jīng)用到了計(jì)算機(jī)軟件系統(tǒng)和硬件系統(tǒng)設(shè)計(jì)的各個(gè)方面。軟硬件等并發(fā)系統(tǒng)規(guī)模的不斷擴(kuò)大，其組成和結(jié)構(gòu)越來(lái)越復(fù)雜，設(shè)計(jì)、分析和開發(fā)并發(fā)系統(tǒng)變得越來(lái)越困難，因此必須對(duì)系統(tǒng)的進(jìn)程進(jìn)行科學(xué)系統(tǒng)的表示，才能保證不斷發(fā)展的系統(tǒng)設(shè)計(jì)與分析的需求。在進(jìn)程交互中，有可見性交互和不可見性交互，本文主要研究可見性研究，并提供區(qū)分可見性研究和不可見性研究的方法。進(jìn)程代數(shù)是一種形式化的描述復(fù)雜并發(fā)系統(tǒng)的建模工具，它是一種高層的描述語(yǔ)言，它是支持并發(fā)分布系統(tǒng)對(duì)的組合描述及其性質(zhì)形式化證明的代數(shù)語(yǔ)言。它以代數(shù)形式來(lái)描述模型，并且為模型化的系統(tǒng)定義了一套完整的語(yǔ)法和語(yǔ)義。隨著計(jì)算機(jī)軟硬件等并發(fā)系統(tǒng)規(guī)模的不斷擴(kuò)大，其組成和結(jié)構(gòu)越來(lái)越復(fù)雜，設(shè)計(jì)、分析和開發(fā)并發(fā)系統(tǒng)變得越來(lái)越困難，因此必須對(duì)系統(tǒng)的進(jìn)程進(jìn)行科學(xué)系統(tǒng)的表示，才能保證不斷發(fā)展的系統(tǒng)設(shè)計(jì)與分析的需求。作為控制并發(fā)系統(tǒng)復(fù)雜度和保證并發(fā)系統(tǒng)設(shè)計(jì)正確性和服務(wù)質(zhì)量的一種有效的手段，形式化方法的研究經(jīng)過(guò)幾十年努力，取得很大成績(jī)，相應(yīng)技術(shù)已經(jīng)用到了計(jì)算機(jī)軟件系統(tǒng)和硬件系統(tǒng)設(shè)計(jì)的各個(gè)方面。二、本課題研究的基本內(nèi)容，擬解決的主要問(wèn)題和難點(diǎn)問(wèn)題1、基本內(nèi)容進(jìn)程之間如何進(jìn)行交互，交互過(guò)程中存在的一系列問(wèn)題及其解決方法，進(jìn)程代數(shù)的結(jié)構(gòu)化操作語(yǔ)義，進(jìn)程之間消息傳遞的可見性和不可見性，找到合適的案例分析，進(jìn)行研究，得出結(jié)論。形式化的方法是在20實(shí)際60年代末期為了解決“軟件危機(jī)”而發(fā)展起來(lái)的，所謂的形式化方法，就是利用具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的刻畫語(yǔ)言和分析技術(shù)來(lái)設(shè)計(jì)、分析、簡(jiǎn)化計(jì)算機(jī)系統(tǒng)。形式化方法可以簡(jiǎn)單地理解為形式化刻畫和形式推理相結(jié)合的一種研究方法。形式刻畫就是要明確描述索要設(shè)計(jì)的系統(tǒng)和其性質(zhì)，通常，系統(tǒng)的刻畫是由一種形式化語(yǔ)言，例如進(jìn)程代數(shù)來(lái)實(shí)現(xiàn)，這種刻畫語(yǔ)言具有嚴(yán)格的語(yǔ)法和語(yǔ)義，用來(lái)表達(dá)系統(tǒng)的功能行為或者內(nèi)部結(jié)構(gòu)等，由于形式刻畫語(yǔ)言具有嚴(yán)格的語(yǔ)法和語(yǔ)義，用來(lái)表達(dá)系統(tǒng)的功能行為或內(nèi)部結(jié)構(gòu)等。因?yàn)樾问娇坍嬀哂袊?yán)格的數(shù)學(xué)基礎(chǔ)，因此，消除模糊性、二義性和不完整性有利于系統(tǒng)的設(shè)計(jì)、分析和簡(jiǎn)化并發(fā)系統(tǒng)，高效的機(jī)械化的系統(tǒng)形式化設(shè)計(jì)、分析和簡(jiǎn)化方法就是它所追求的目標(biāo)。作為控制并發(fā)系統(tǒng)復(fù)雜度和保證并發(fā)系統(tǒng)設(shè)計(jì)正確性和服務(wù)質(zhì)量的一種有效的手段，形式化方法的研究經(jīng)過(guò)幾十年努力，取得很大成績(jī)，相應(yīng)技術(shù)已經(jīng)用到了計(jì)算機(jī)軟件系統(tǒng)和硬件系統(tǒng)設(shè)計(jì)的各個(gè)方面。2、擬解決的主要問(wèn)題（1）形式化操作語(yǔ)義描述進(jìn)程交互；（2）區(qū)分進(jìn)程交互的可見性和不可見性。3、難點(diǎn)問(wèn)題內(nèi)部動(dòng)作和外部動(dòng)作的區(qū)別。三、研究步驟、方法及措施1、仔細(xì)研究文獻(xiàn)6,學(xué)會(huì)進(jìn)程演算的操作語(yǔ)義；2、了解進(jìn)程之間進(jìn)行交互的動(dòng)作；3、認(rèn)識(shí)基本事件結(jié)構(gòu)以及四元組；4、研究進(jìn)程之間消息傳遞的可見性和不可見性；當(dāng)進(jìn)程交互加密時(shí)是不可見的，當(dāng)進(jìn)程交互消息可以被第三方看見時(shí)，是可見的。5、舉例分析，得出結(jié)論。四、工作進(jìn)度序號(hào)設(shè)計(jì)（論文）各階段名稱日期1查閱、學(xué)習(xí)文獻(xiàn)資料，結(jié)合已學(xué)過(guò)的課程，明確對(duì)應(yīng)的理論、方法、步驟、撰寫開題報(bào)告1～2周2畢業(yè)實(shí)習(xí)，撰寫實(shí)習(xí)、開題報(bào)告3～5周3分析交互進(jìn)程特征6～7周4研究形式語(yǔ)言刻畫交互消息可見與不可見的進(jìn)程行為8～9周5給出交互消息可見的進(jìn)程表示及應(yīng)用實(shí)例分析10～11周6撰寫畢業(yè)論文，完成論文初稿12～13周7畢業(yè)論文修改定稿14～15周8完成文獻(xiàn)翻譯，準(zhǔn)備做好答辯16～17周9答辯資料整理，論文再一次修改，提交存檔18周五、主要參考文獻(xiàn)[1]黃建新,李群,余文廣,王維平.基于線程的進(jìn)程交互仿真框架研究[J].系統(tǒng)仿真報(bào),2011,23(4):652-658.[2]蔣新華,王中杰,吳啟迪,余有靈.進(jìn)程交互仿真機(jī)制的多線程實(shí)現(xiàn)及其應(yīng)用[J].

計(jì)算機(jī)仿真,2004,21(11):228-231.[3]馮惠軍,馮允成.離散事件仿真模型的實(shí)現(xiàn)方法[J].石家莊鐵道學(xué)院學(xué)報(bào),1995,22(03):48-55.[4]馬富銀,吳偉蔚.交互仿真技術(shù)[J].機(jī)械設(shè)計(jì)與研究,2010,20(06):75-77.[5]李群,黃建新,賈全,王維平,朱一凡.基于進(jìn)程的Agent體系仿真模型框架[J].系統(tǒng)仿真學(xué)報(bào),2011,23(11):2475-2481.[6]王永祥.進(jìn)程代數(shù)[M].北京:科學(xué)出版社,2007.[7]余文廣,王維平,柏永斌,李群.基于多進(jìn)程的Agent行為描述及其仿真調(diào)度研究[J].系統(tǒng)仿真學(xué)報(bào),2012,24(03):509-514+520.[8]黃建新.基于ABMS的體系效能仿真評(píng)估方法研究[D].2011.[9]vanGlabbeekRJ,GoltzU.Refinementofactionsandequivalencenotionsforconcurrentsystems[J].ActaInformatica,2001,37(4/5):229-327.[10]JiangJ,WuJ.Thepreservationofinterleavingequivalences[C].Proceedingsofthe10thIEEEInternationalConferenceonEngineeringofComplexComputerSystems.IEEEComputerSocietyPress,2005,580-589.

六