面向服務(wù)計(jì)算的拜占庭容錯(cuò)協(xié)議

　　針對(duì)現(xiàn)有拜占庭容錯(cuò)協(xié)議的假設(shè)（要求被保護(hù)的對(duì)象是被動(dòng)的和獨(dú)立的）不適用于服務(wù)計(jì)算等新興計(jì)算模型的問(wèn)題，提出一種面向服務(wù)計(jì)算的拜占庭容錯(cuò)協(xié)議。該協(xié)議在服務(wù)請(qǐng)求方和服務(wù)提供方兩端均創(chuàng)建服務(wù)復(fù)制品，采用基于狀態(tài)機(jī)的主動(dòng)復(fù)制技術(shù)，在服務(wù)復(fù)制品間進(jìn)行三輪通信，就該請(qǐng)求的編號(hào)和內(nèi)容達(dá)成一致，隨后該請(qǐng)求被提交給上層應(yīng)用邏輯處理；收到應(yīng)答后，服務(wù)請(qǐng)求方的復(fù)制品進(jìn)行三輪通信就應(yīng)答的編號(hào)和內(nèi)容達(dá)成一致后接受該應(yīng)答。針對(duì)現(xiàn)有面向服務(wù)計(jì)算的拜占庭容錯(cuò)協(xié)議只有簡(jiǎn)單的正確性推理缺乏形式化驗(yàn)證的問(wèn)題，采用1/0自動(dòng)機(jī)和模擬關(guān)系方法進(jìn)行正確性證明，更加嚴(yán)謹(jǐn)和正式。構(gòu)造一個(gè)高度抽象的簡(jiǎn)單1/0自動(dòng)機(jī)S，此自動(dòng)機(jī)滿足安全性和及時(shí)性；將協(xié)議中的各方分解成若干簡(jiǎn)單1/0自動(dòng)機(jī)：前端自動(dòng)機(jī)、后端自動(dòng)機(jī)和多播通道自動(dòng)機(jī)；最后用模擬關(guān)系方法證明各成員自動(dòng)機(jī)構(gòu)成的系統(tǒng)實(shí)現(xiàn)了自動(dòng)機(jī)S，從而證明協(xié)議的正確性。使用1/0自動(dòng)機(jī)可以精確描述協(xié)議，以此為基礎(chǔ)進(jìn)行證明比感性推理的證明方法更加規(guī)范。