本文選題：觀察者模式 + 實(shí)時(shí)系統(tǒng)　； 參考：《計(jì)算機(jī)科學(xué)》2017年12期

【摘要】：復(fù)雜實(shí)時(shí)系統(tǒng)的驗(yàn)證問題一直備受關(guān)注。驗(yàn)證過程中,驗(yàn)證特性可以用時(shí)序邏輯來描述,但時(shí)序邏輯對于非專業(yè)人員而言較為復(fù)雜,難度較大。觀察者模式是一個(gè)額外的子系統(tǒng),可以將復(fù)雜的驗(yàn)證特性轉(zhuǎn)換為簡單的可達(dá)性問題,同時(shí)也可以避免使用復(fù)雜的驗(yàn)證算法。將Etienne和Nouha Abid等人提出的抽象的觀察者模式應(yīng)用到實(shí)時(shí)系統(tǒng)實(shí)例——Train-Gate系統(tǒng)中,采用UPPAAL工具對Train-Gate系統(tǒng)中的某些場景建立觀察者模型,并采用對比實(shí)驗(yàn)將驗(yàn)證結(jié)果與無觀察者模式狀態(tài)下的驗(yàn)證結(jié)果進(jìn)行對比。對比結(jié)果表明,使用觀察者模式和驗(yàn)證特性都可以得到正確的驗(yàn)證結(jié)果,但觀察者更節(jié)省時(shí)間,對于非專業(yè)人員而言更簡單且更容易接受。因此,使用觀察者模式對如TrainGate的實(shí)時(shí)系統(tǒng)進(jìn)行驗(yàn)證是可行的。
[Abstract]:The verification of complex real-time systems has attracted much attention. In the process of verification, the characteristics of verification can be described by temporal logic, but temporal logic is more complex and difficult for non-professionals. Observer pattern is an additional subsystem that can transform complex verification features into simple reachability problems while avoiding the use of complex verification algorithms. The abstract observer model proposed by Etienne and Nouha Abid is applied to the real time system, Train-Gate system, and the observer model of some scenes in Train-Gate system is established by UPPAAL tool. The verification results are compared with those in the no-observer mode by contrast experiments. The comparison results show that the correct results can be obtained by using both the observer mode and the validation feature, but the observer saves more time and is simpler and easier to accept for non-professionals. Therefore, it is feasible to validate real-time systems such as TrainGate using observer mode.
【作者單位】： 四川大學(xué)計(jì)算機(jī)學(xué)院;
【基金】：四川省應(yīng)用基礎(chǔ)研究項(xiàng)目:嵌入式系統(tǒng)軟件形式化驗(yàn)證技術(shù)研究(2014JY0112)資助
【分類號】：TP301.1

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李華春;實(shí)時(shí)系統(tǒng)中設(shè)備并行應(yīng)滿足的條件[J];計(jì)算機(jī)工程;1984年01期

2 劉惠義,秦益,鄭曉東;Windows2000/NT環(huán)境下實(shí)時(shí)系統(tǒng)的開發(fā)[J];計(jì)算機(jī)與現(xiàn)代化;2004年04期

3 張利飛,孫西全,張?jiān)录t;分布式實(shí)時(shí)系統(tǒng)結(jié)構(gòu)研究[J];現(xiàn)代計(jì)算機(jī)(專業(yè)版);2005年08期

4 張志余;;實(shí)時(shí)系統(tǒng)的語言特征[J];航空計(jì)算技術(shù);1990年03期

5 楊則正;實(shí)時(shí)系統(tǒng)設(shè)計(jì)、調(diào)試和評價(jià)方法[J];管理科學(xué)文摘;1996年03期

6 Sarah;;網(wǎng)上炒股好幫手——康熙證券實(shí)時(shí)系統(tǒng)[J];世界計(jì)算機(jī)周刊;1999年01期

7 毛羽剛,金士堯,張擁軍,胡華平;分布強(qiáng)實(shí)時(shí)系統(tǒng)的可預(yù)測性研究[J];計(jì)算機(jī)研究與發(fā)展;2000年06期

8 王文,于戈,王彩榮;一種分布式實(shí)時(shí)系統(tǒng)的支撐平臺[J];東北大學(xué)學(xué)報(bào);2002年03期

9 趙嶺忠,董榮勝,蔡國永,古天龍;基于對象分布式實(shí)時(shí)系統(tǒng)約束的一致性研究[J];計(jì)算機(jī)工程與應(yīng)用;2002年15期

10 劉瑞成;張立臣;;實(shí)時(shí)系統(tǒng)的面向方面模型[J];計(jì)算機(jī)工程與設(shè)計(jì);2006年06期

相關(guān)會議論文 前7條

1 李亞茹;;國華太電生產(chǎn)實(shí)時(shí)系統(tǒng)的幾項(xiàng)應(yīng)用開發(fā)[A];二○○九年全國電力企業(yè)信息化大會論文集[C];2009年

2 胡光明;蘇冉冉;劉利;;強(qiáng)實(shí)時(shí)系統(tǒng)高程數(shù)據(jù)庫設(shè)計(jì)方法[A];第五屆中國衛(wèi)星導(dǎo)航學(xué)術(shù)年會論文集-S8 衛(wèi)星導(dǎo)航模型與方法[C];2014年

3 鄒沐昌;趙北光;;分布式實(shí)時(shí)系統(tǒng)中控制模型及其堅(jiān)定性研究[A];1992年中國控制與決策學(xué)術(shù)年會論文集[C];1992年

4 畢小龍;王洪躍;朱大海;徐治皋;;基于COM+組件的電站實(shí)時(shí)系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)[A];2004電站自動化信息化學(xué)術(shù)技術(shù)交流會議論文集[C];2004年

5 陳耀;李慕君;馮志彪;;基于MATLAB的單機(jī)實(shí)時(shí)系統(tǒng)的應(yīng)用研究[A];2004全國測控、計(jì)量與儀器儀表學(xué)術(shù)年會論文集（上冊）[C];2004年

6 周國祥;石雷;韓江洪;;一種實(shí)時(shí)系統(tǒng)中實(shí)現(xiàn)軟件仿真模擬測試的方法[A];計(jì)算機(jī)技術(shù)與應(yīng)用進(jìn)展——全國第17屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用（CACIS）學(xué)術(shù)會議論文集（上冊）[C];2006年

7 嚴(yán)雋薇;宋國斌;張克技;;一種實(shí)時(shí)系統(tǒng)分析法——H-P擴(kuò)展法[A];第三屆全國控制與決策系統(tǒng)學(xué)術(shù)會議論文集[C];1991年

相關(guān)重要報(bào)紙文章 前2條

1 廣東省電信科學(xué)技術(shù)研究院多媒體部 張宇飛 盧燕青;實(shí)時(shí)系統(tǒng)軟件分析和設(shè)計(jì)方法綜述[N];中國計(jì)算機(jī)報(bào);2000年

2 ;可信賴的生產(chǎn)幫手[N];中國冶金報(bào);2002年

相關(guān)博士學(xué)位論文 前7條

1 王璽;實(shí)時(shí)系統(tǒng)的基于優(yōu)先級的實(shí)時(shí)重構(gòu)和不基于優(yōu)先級的條件剝奪調(diào)度算法[D];西安電子科技大學(xué);2016年

2 陳艾;面向能耗優(yōu)化的分布式實(shí)時(shí)系統(tǒng)調(diào)度算法研究[D];中國科學(xué)技術(shù)大學(xué);2007年

3 姬孟洛;實(shí)時(shí)系統(tǒng)最差情況執(zhí)行時(shí)間分析的研究[D];國防科學(xué)技術(shù)大學(xué);2006年

4 何忠政;分布式實(shí)時(shí)系統(tǒng)任務(wù)容錯調(diào)度優(yōu)化算法研究[D];哈爾濱工程大學(xué);2016年

5 譚朋柳;開放式實(shí)時(shí)系統(tǒng)任務(wù)調(diào)度的研究[D];華中科技大學(xué);2008年

6 王立剛;開放式混合實(shí)時(shí)系統(tǒng)中的調(diào)度方法研究[D];中國科學(xué)技術(shù)大學(xué);2006年

7 朱響斌;開放式實(shí)時(shí)Linux的研究與設(shè)計(jì)[D];復(fù)旦大學(xué);2005年

相關(guān)碩士學(xué)位論文 前10條

1 宋曉敏;實(shí)時(shí)系統(tǒng)的測試方法研究與應(yīng)用[D];青島科技大學(xué);2015年

2 王思琪;基于時(shí)序故障樹的實(shí)時(shí)系統(tǒng)安全性驗(yàn)證方法研究[D];南京航空航天大學(xué);2016年

3 馮博洋;基于模型的實(shí)時(shí)系統(tǒng)形式化驗(yàn)證方法研究與實(shí)現(xiàn)[D];杭州電子科技大學(xué);2016年

4 韋楊毅;“礦井北斗”精準(zhǔn)安全管理系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];北京交通大學(xué);2017年

5 向智林;基于軟件能力成熟度模型的實(shí)時(shí)系統(tǒng)開發(fā)過程研究[D];廣東工業(yè)大學(xué);2005年

6 羅秉安;軟件能力成熟度模型在實(shí)時(shí)系統(tǒng)開發(fā)中的應(yīng)用[D];廣東工業(yè)大學(xué);2003年

7 張穩(wěn);模糊Petri網(wǎng)在實(shí)時(shí)系統(tǒng)中的應(yīng)用研究[D];華東師范大學(xué);2006年

8 陳艷;并發(fā)實(shí)時(shí)系統(tǒng)的模型及其形式化[D];廣西師范大學(xué);2008年

9 趙天慧;網(wǎng)格環(huán)境下異構(gòu)動態(tài)分布式實(shí)時(shí)系統(tǒng)的面向方面的資源模型[D];廣東工業(yè)大學(xué);2008年

10 徐敏;分布式實(shí)時(shí)系統(tǒng)的時(shí)序分析方法研究[D];南京航空航天大學(xué);2011年

，

本文編號：1817268