本文選題：軟件逐步精化　切入點：精化驗證　出處：《上海大學》2016年博士論文　論文類型：學位論文

【摘要】：軟件精化技術是軟件形式方法的基石之一,是保證軟件可靠性的重要手段。精化技術可分為逐步精化和精化驗證。逐步精化用于遞增式開發(fā),通過逐步引入細節(jié)來降低開發(fā)復雜度以及保證引入細節(jié)前后的一致性。精化驗證用于實現(xiàn)的正確性驗證,許多程序驗證問題都可以歸結為精化驗證。從上世紀七十年代起,人們已對精化技術開展了大量研究。然而在智能體系統(tǒng)、軟件事務內(nèi)存以及弱內(nèi)存存儲模型中,精化關系變得更加復雜,使得驗證更加困難�，F(xiàn)有的研究工作尚有許多問題亟待解決。本文在對多智能體系統(tǒng)的逐步精化、軟件事務內(nèi)存和寫全序弱內(nèi)存模型的精化驗證方面進行了研究,主要工作和創(chuàng)新點如下。1、對情景化多智能體系統(tǒng)的逐步精化進行研究。由于情景化多智能體系統(tǒng)本身具有的復雜性,人們從宏觀、中間及微觀三個不同的層次來進行開發(fā),為了保證層次之間及層次內(nèi)的一致性,開發(fā)過程中采用形式的遞增式開發(fā)方法是必要的。在中間層次上,當引入新的智能體時,我們采用Object-Z表示法對系統(tǒng)進行規(guī)格說明描述,并且給出基于Object-Z表示法和活動系統(tǒng)跡語義的精化證明責任。宏觀層次到中間層次的轉(zhuǎn)換,從用時間段謂詞描述的宏觀層次規(guī)格說明出發(fā),給出帶有時間段謂詞的規(guī)格說明的精化方法,逐步從宏觀層次精化為中間層次。2、對軟件事務內(nèi)存實現(xiàn)正確性的精化驗證進行了研究。首先簡述了事務內(nèi)存規(guī)格說明1準則(Transactional Memory Specification 1,TMS1)及軟件事務內(nèi)存實現(xiàn)TL2-RCAD。針對交換性和引入簡單預言變量的前向模擬這兩種驗證方法不能驗證TL2-RCAD正確性的問題,提出了語義交換的驗證方法,給出了證明責任,使得一類這兩種方法不能驗證的軟件事務內(nèi)存實現(xiàn)得到驗證。3、給出寫全序弱內(nèi)存模型新操作語義、編譯優(yōu)化和局部程序轉(zhuǎn)換規(guī)則的正確性驗證。在寫全序弱內(nèi)存模型上,分析了現(xiàn)有操作語義和公理語義的不足,給出了新公理語義以及在此基礎上定義的新操作語義,證明了新公理語義和原公理語義的等價性,以及新操作語義與新公理語義的等價性。在新操作語義的基礎上,驗證了寫全序弱內(nèi)存模型上的編譯優(yōu)化以及局部程序轉(zhuǎn)換規(guī)則的正確性。4、針對目前提出的寫全序弱內(nèi)存模型上線性化定義的不足,定義了一個僅使用調(diào)用返回接口的新線性化概念,并且證明該線性化與上下文精化之間的等價性,給出了弱內(nèi)存模型上原子性的規(guī)格說明。5、為模塊化的驗證寫全序弱內(nèi)存模型上線性化,提出基于依賴保證的模擬,給出該模擬保證精化關系的正確性證明。分析了寫全序弱內(nèi)存模型上的循環(huán)鎖、票循環(huán)鎖、讀-拷貝-更新實現(xiàn),給出原子性的規(guī)格說明,并驗證具體實現(xiàn)與規(guī)格說明之間的線性化關系。
[Abstract]:Software refinement is one of the cornerstones of software formal methods and an important means to ensure the reliability of software. By gradually introducing details to reduce development complexity and ensure consistency before and after the introduction of details. Refined verification is used to verify the correctness of the implementation, many program verification problems can be attributed to refined verification. A lot of research has been done on the refinement technology. However, in the agent system, software transaction memory and weak memory storage model, the elaboration relationship becomes more complex. It makes verification more difficult. There are still many problems to be solved. In this paper, we study the refinement of multi-agent system, the refinement verification of software transaction memory and write full order weak memory model. The main work and innovations are as follows: 1. The gradual refinement of situational multi-agent system is studied. Because of the complexity of situational multi-agent system, people develop it from three different levels: macro, middle and micro. In order to ensure the consistency between and within the levels, it is necessary to adopt the formal incremental development method in the development process. At the middle level, when introducing new agents, we use Object-Z representation to describe the system specifications. The responsibility of proof based on Object-Z representation and the semantics of active system trace is given. The transformation from macro level to middle level is based on the specification of macro level described by time period predicate. A refined method for specification with time period predicates is given. In this paper, the verification of the correctness of software transaction memory implementation is studied from macro level refinement to intermediate level. Firstly, the transaction memory specification (1) criterion and the software transaction memory implementation (TL2-RCAD) are briefly introduced in this paper, which include the Transactional Memory memory specification 1 (1) and the software transaction memory implementation (TL2-RCAD). The two verification methods, commutativity and forward simulation with simple predictive variables, cannot verify the correctness of TL2-RCAD. In this paper, a verification method of semantic exchange is proposed, and the burden of proof is given, which verifies a class of software transaction memory implementations that cannot be verified by these two methods. The new operation semantics of write full order weak memory model are given. In this paper, the shortcomings of the existing operation semantics and axiom semantics are analyzed, and the new axiom semantics and the new operation semantics defined on this basis are given. The equivalence between the new axiom semantics and the primitive axiom semantics, and the equivalence between the new operation semantics and the new axiom semantics are proved. The correctness of compiling optimization and local program conversion rules on write full order weak memory model is verified. 4. Aiming at the deficiency of linearization definition on write full order weak memory model, A new linearization concept using only the calling return interface is defined, and the equivalence between this linearization and contextual refinement is proved. In this paper, the specification of atomicity on weak memory model is given. 5. Linearization of full order weak memory model for modularized verification is presented, and the simulation based on dependency guarantee is proposed. The correctness of the simulation to ensure the elaboration relationship is proved. The cyclic lock, ticket cyclic lock, read copy update implementation on the write order weak memory model are analyzed, and the atomic specification is given. The linearization relationship between specification and specification is verified.
【學位授予單位】：上海大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP311.1

【相似文獻】

相關期刊論文 前6條

1 祁方民;;Petri網(wǎng)結點精化及其應用[J];計算機與現(xiàn)代化;2014年07期

2 王云峰 ,龐軍 ,查鳴 ,楊朝暉 ,鄭國梁;精化演算支撐工具的分析[J];計算機應用與軟件;2002年02期

3 劉瑜,張世琨,鄔倫,葉燕林;地理信息系統(tǒng)中的設計模式——以過濾和精化為例[J];北京大學學報(自然科學版);2001年06期

4 熊建;陳曉克;;基于Wiki技術可持續(xù)精化精品課教學平臺[J];福建電腦;2010年12期

5 楊朝暉;王云峰;鄭國梁;;精化演算支撐工具PRT的研究[J];計算機科學;2000年03期

6 ;[J];;年期

相關會議論文 前5條

1 周鑫;;面對新形勢、樹立新觀念、迎接新挑戰(zhàn)——談企業(yè)職工面對“精化分立、分業(yè)經(jīng)營”新形勢的感想[A];陜西省體制改革研究會2006-2007優(yōu)秀論文集[C];2007年

2 高陽;王敏中;;拉伸矩形梁的精化理論[A];北京力學會第11屆學術年會論文摘要集[C];2005年

3 高陽;王敏中;;橫觀各項同性壓電矩形直梁的精化理論[A];中國力學學會學術大會'2005論文摘要集（下）[C];2005年

4 趙紅麗;范景輝;郭小方;劉廣;陳建平;;CR輔助的基線參數(shù)精化方法研究[A];第十七屆中國遙感大會摘要集[C];2010年

5 江東;王慶賓;王凱;;重力場精化的空間插值方法研究[A];中國測繪學會2010年學術年會論文集[C];2010年

相關重要報紙文章 前10條

1 羅平華;彩虹精化氣霧漆龍頭今日掛牌[N];證券時報;2008年

2 證券時報記者 羅平華;彩虹精化出口收入逆勢增長三成[N];證券時報;2009年

3 證券時報記者 向南;彩虹精化 涉足室內(nèi)環(huán)保業(yè)務[N];證券時報;2010年

4 記者 翟敏;彩虹精化上半年業(yè)績平平 管理層就“巨額訂單”事件致歉[N];上海證券報;2011年

5 記者 王健杰;彩虹精化營收內(nèi)降外增[N];北京商報;2009年

6 中國空空導彈研究院 綜合管理處;精化軍品能力 優(yōu)化民品結構[N];中國航空報;2004年

7 本報通訊員 周善良 記者 李雨農(nóng);精化分立 一所多制[N];中國航空報;2002年

8 武連寅邋蔡軍;淮化精化再次入選國家高新企業(yè)[N];中國化工報;2007年

9 記者 孫燕飚　劉瓊;萬潤精化再上會 日德企業(yè)“鎖喉”難改觀[N];第一財經(jīng)日報;2011年

10 記者 況玉清;彩虹精化虛假陳述案下月開庭[N];北京商報;2012年

相關博士學位論文 前5條

1 李壯;軟件逐步精化及并發(fā)程序精化驗證[D];上海大學;2016年

2 陳桂芝;解大規(guī)模非對稱矩陣特征問題的一些精化算法[D];大連理工大學;2000年

3 梁紅瑾;并發(fā)程序精化驗證及其應用[D];中國科學技術大學;2014年

4 牛大田;計算大規(guī)模矩陣部分奇異值分解的精化Lanczos型算法[D];大連理工大學;2003年

5 梁坤;高靈敏度GPS接收技術中幾個關鍵問題的研究[D];中國科學院研究生院（國家天文臺）;2008年

相關碩士學位論文 前7條

1 錢潔;軌旁系統(tǒng)的形式化建模精化與驗證[D];華東師范大學;2015年

2 王玲;模型精化過程中模型間一致性檢測研究[D];華東師范大學;2016年

3 陳穎;特殊正交各向異性壓電板的精化理論[D];遼寧科技大學;2016年

4 劉穩(wěn);隱式重啟和精化的全局Lanczos方法與塊Lanczos方法[D];南京航空航天大學;2014年

5 劉婷婷;雙層梁的精化理論[D];遼寧科技大學;2015年

6 付亞軍;面向多主體的基于政策的運行機制研究[D];湖南大學;2009年

7 吳鋼;解大規(guī)模非對稱矩陣特征問題Lanczos方法的兩種精化版本[D];大連理工大學;2001年

，

本文編號：1594115