【摘要】：Event-B是一種基于集合論和謂詞邏輯的形式化系統(tǒng)語言,能夠采用精化策略為系統(tǒng)建立逐漸精化的模型。提出了如何將Event-B應(yīng)用到實(shí)際工業(yè)領(lǐng)域的方法,包括重寫需求、建立抽象模型及逐層精化三個(gè)步驟。首先從環(huán)境、功能、性質(zhì)三個(gè)主要方面重寫需求,明確精化策略;然后利用形式化方法建立抽象模型并驗(yàn)證該模型;最后,在正確的抽象模型上按照精化策略添加需求、逐層精化,并對(duì)每層模型進(jìn)行驗(yàn)證,基于滿足需求的最后一層模型,可進(jìn)一步利用工具完成代碼自動(dòng)生成。該方法學(xué)采用精化理論,以逐層遞增的方式明確被開發(fā)系統(tǒng)的需求及性質(zhì),并進(jìn)行形式化建模與驗(yàn)證,確保了模型的正確性。為了說明該方法學(xué)的可行性,以真正工業(yè)界的多應(yīng)用智能卡為實(shí)例,基于Event-B方法及其工具平臺(tái)Rodin給出了該方法在實(shí)際建模及驗(yàn)證過程中的應(yīng)用。
[Abstract]:Event-B is a formal system language based on set theory and predicate logic. This paper presents a method of applying Event-B to the practical industrial field, which includes three steps: rewriting requirements, building abstract model and refining layer by layer. Firstly, the requirements are rewritten from three main aspects: environment, function and nature. Then the abstract model is established by formal method and the model is verified. Finally, the requirements are added to the correct abstract model according to the refined strategy. Layer by layer refinement and verification of each layer model, based on the last layer model to meet the requirements, we can further use tools to complete the automatic generation of code. The methodology uses the refined theory to clarify the requirements and properties of the developed system in a hierarchical incremental manner, and formalizes and verifies the model to ensure the correctness of the model. In order to illustrate the feasibility of the methodology, the application of this method in the process of modeling and verification is given based on the Event-B method and its tool platform Rodin, taking the real industrial multi-application smart card as an example.
【作者單位】： 華東師范大學(xué)教育部軟硬件協(xié)同設(shè)計(jì)技術(shù)與應(yīng)用工程研究中心;信息網(wǎng)絡(luò)安全公安部重點(diǎn)實(shí)驗(yàn)室;上海市社會(huì)保障卡服務(wù)中心;
【基金】：國家自然科學(xué)基金資助項(xiàng)目(91118008) 國家973計(jì)劃資助項(xiàng)目(2011CB302904) 上海市科委資助項(xiàng)目(12511504205) 信息網(wǎng)絡(luò)安全公安部重點(diǎn)實(shí)驗(yàn)室開放課題資助項(xiàng)目(C12604) 上海高校知識(shí)服務(wù)平臺(tái)-可信物聯(lián)網(wǎng)產(chǎn)學(xué)研聯(lián)合研發(fā)中心(籌)資助項(xiàng)目
【分類號(hào)】：TP368.1

【參考文獻(xiàn)】

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

1 綦艷霞;沈慧麗;陳朝暉;顧斌;;SPARDL模型的Event-B解釋[J];計(jì)算機(jī)應(yīng)用;2012年12期

2 雷洋;胡曉輝;陳永;李欣;;基于Event-B的列車車載控制器系統(tǒng)的形式化建模[J];數(shù)字技術(shù)與應(yīng)用;2012年08期

【共引文獻(xiàn)】

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

1 胡曉輝;肖知屹;陳永;李欣;;列車安全距離控制形式化建模與驗(yàn)證[J];計(jì)算機(jī)應(yīng)用;2014年03期

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

1 權(quán)慶樂;基于Agent的智能分布式實(shí)時(shí)監(jiān)控系統(tǒng)通信機(jī)制的形式化研究[D];蘭州交通大學(xué);2013年

【相似文獻(xiàn)】

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

1 章s，

本文編號(hào)：2138757