本文選題：多形態(tài)時(shí)鐘 + 標(biāo)號(hào)遷移系統(tǒng)�。� 參考：《華東師范大學(xué)》2017年博士論文

【摘要】：缺乏系統(tǒng)的科學(xué)的測(cè)試體系是一直以來(lái)影響安全軟件測(cè)試可信度的根本問(wèn)題。在現(xiàn)有的工程實(shí)踐中,測(cè)試是實(shí)驗(yàn)性行為的認(rèn)知和實(shí)施方案普遍存在,威脅著系統(tǒng)的安全性并且這一問(wèn)題隨著安全軟件需求量的激增,職責(zé)范圍的外延,規(guī)模的擴(kuò)大和復(fù)雜度的提高變得越來(lái)越嚴(yán)重。因此,構(gòu)造高效可信的安全測(cè)試方法和工具已經(jīng)成為安全軟件行業(yè)不可回避的挑戰(zhàn)。本文以構(gòu)建安全軟件的安全性測(cè)試?yán)碚摽蚣芗捌鋺?yīng)用為主要研究目標(biāo),針對(duì)安全軟件苛求質(zhì)量的實(shí)際需求,以形式化測(cè)試為基礎(chǔ),根據(jù)安全軟件的典型特征,從設(shè)計(jì)符合其特點(diǎn)的建模語(yǔ)言開(kāi)始,構(gòu)建了統(tǒng)一安全性驗(yàn)證和安全性測(cè)試的理論框架。該理論框架立足于研發(fā)安全軟件的全流程而非純粹測(cè)試的立場(chǎng),在保證測(cè)試方法本身正確性的同時(shí),設(shè)計(jì)了通過(guò)測(cè)試也可以證明軟件實(shí)現(xiàn)是安全的理論框架和相應(yīng)的測(cè)試序列生成方法,主要貢獻(xiàn)體現(xiàn)在:1.定義了多形態(tài)時(shí)鐘時(shí)間模型,設(shè)計(jì)了多形態(tài)時(shí)鐘輸入輸出遷移系統(tǒng),給出了相應(yīng)語(yǔ)法和語(yǔ)義的形式化定義,提出了將時(shí)間模型從系統(tǒng)行為模型中分離出來(lái)的安全軟件建模方法;2.提出了統(tǒng)一的安全性驗(yàn)證與測(cè)試序列生成理論框架。該理論框架站在安全軟件全流程而非單一測(cè)試的角度,將對(duì)規(guī)約設(shè)計(jì)的安全性驗(yàn)證與軟件實(shí)現(xiàn)的安全性測(cè)試融合在同一個(gè)理論框架中,證明了如果某個(gè)實(shí)現(xiàn)通過(guò)了基于滿足安全性屬性模型所生成的測(cè)試序列集合,那么該實(shí)現(xiàn)也滿足期望的安全性屬性的結(jié)論,并給出了相應(yīng)的測(cè)試序列生成方法;3.構(gòu)建了多形態(tài)時(shí)鐘輸入輸出遷移系統(tǒng)的安全性測(cè)試方法,定義了多形態(tài)時(shí)鐘輸入輸出一致性關(guān)系,設(shè)計(jì)了相應(yīng)的符號(hào)測(cè)試方法。并在此基礎(chǔ)上,為了滿足安全軟件防護(hù)能力測(cè)試的需求,進(jìn)一步提出了采用規(guī)約變異的測(cè)試方法計(jì)算安全軟件的故障測(cè)試序列集合,定義了基于安全故障模型的變異算子,給出了基于弱變異思想的誘導(dǎo)規(guī)則,設(shè)計(jì)了k周期誘導(dǎo)算法。為了展示方法的可行性,本文以某實(shí)際車(chē)載列車(chē)自動(dòng)防護(hù)軟件系統(tǒng)為例說(shuō)明了基于多形態(tài)時(shí)鐘輸入輸出遷移系統(tǒng)的安全測(cè)試?yán)碚撛诎踩浖到y(tǒng)中的具體應(yīng)用。
[Abstract]:The lack of systematic and scientific testing system is the fundamental problem that affects the reliability of security software testing. In existing engineering practice, testing is a widespread cognitive and implementation scheme of experimental behavior, threatening the security of the system and increasing the demand for security software and the extension of the scope of responsibility. The enlargement of scale and the increase of complexity become more and more serious. Therefore, the construction of efficient and credible security testing methods and tools has become an unavoidable challenge in the security software industry. The main research goal of this paper is to construct the security testing theory framework and its application of security software, aiming at the practical requirement of demanding quality of security software, based on formal testing, according to the typical characteristics of security software. Starting with the design of modeling language which conforms to its characteristics, the theoretical framework of unified security verification and security testing is constructed. The theoretical framework is based on the position of developing the whole process of security software rather than pure testing, while ensuring the correctness of the test method itself. It can also be proved by testing that the software implementation is a safe theoretical framework and a corresponding test sequence generation method. The main contribution is reflected in: 1. The multi-morphological clock time model is defined, the multi-morphological clock input / output migration system is designed, the formal definitions of syntax and semantics are given, and the security software modeling method is proposed, which separates the time model from the system behavior model. A unified theoretical framework for security verification and test sequence generation is proposed. The theoretical framework is based on the whole process of security software rather than a single test, and combines the security verification of protocol design and the security test of software implementation in the same theoretical framework. It is proved that if an implementation passes the set of test sequences generated based on the satisfied security attribute model, then the implementation also satisfies the expected security attribute, and the corresponding test sequence generation method is given. The security test method of multi-morphological clock input / output migration system is constructed. The consistency relationship of multi-morphological clock input and output is defined and the corresponding symbol testing method is designed. On this basis, in order to meet the requirements of security software protection capability testing, a test method of protocol mutation is proposed to calculate the fault test sequence set of security software, and a mutation operator based on security fault model is defined. The induction rule based on weak mutation is given, and the k-period induction algorithm is designed. In order to demonstrate the feasibility of the method, this paper illustrates the application of the security test theory based on the multi-form clock input and output migration system in the security software system, taking an actual on-board train automatic protection software system as an example.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2017
【分類(lèi)號(hào)】：TP311.53

【相似文獻(xiàn)】

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

1 ;輸入輸出[J];電子計(jì)算機(jī)參考資料;1975年Z2期

2 ;張?zhí)烀鞯劝l(fā)明筆序碼 輸入輸出與檢索三統(tǒng)一[J];中文信息;1996年02期

3 肖麗萍，李兢，吳長(zhǎng)奇;C及C＋＋輸入輸出機(jī)制的討論──從庫(kù)函數(shù)到流[J];計(jì)算機(jī)工程與設(shè)計(jì);1996年04期

4 黃軒;編程中輸入輸出技巧的探討[J];現(xiàn)代計(jì)算機(jī);1996年06期

5 ;基本的輸入輸出技術(shù)和部件[J];電訊技術(shù);1981年03期

6 張春華;李迪;翟振坤;鄭炳坤;;輸入輸出延時(shí)對(duì)控制性能的影響分析[J];計(jì)算機(jī)測(cè)量與控制;2013年01期

7 石春剛;王俊;張軍鋒;侯風(fēng)巍;;基于全生命周期的輸入輸出管控研究[J];信息安全與通信保密;2012年12期

8 ;輸入輸出:即將到來(lái)的誘惑[J];微電腦世界;1999年07期

9 ;所見(jiàn)即所得——Adobe Photoshop 5.0應(yīng)用色彩管理輸入輸出相一致[J];每周電腦報(bào);1998年50期

10 傅澄宇;;Teststand中數(shù)字輸入輸出的測(cè)控編程[J];信息技術(shù);2013年12期

相關(guān)會(huì)議論文 前2條

1 楊振宇;陳宗基;;混合系統(tǒng)的一類(lèi)混合輸入輸出自動(dòng)機(jī)模型[A];1997年中國(guó)控制會(huì)議論文集[C];1997年

2 李凡長(zhǎng);;人的n-維信息輸入輸出數(shù)學(xué)模型[A];第一屆全國(guó)人—機(jī)—環(huán)境系統(tǒng)工程學(xué)術(shù)會(huì)議論文集[C];1993年

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

1 小丹;關(guān)于3GIO的問(wèn)答[N];中國(guó)電子報(bào);2002年

2 SuHongXiao;精心配置，提高系統(tǒng)速度[N];電腦報(bào);2004年

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

1 孫海英;基于多形態(tài)時(shí)鐘輸入輸出遷移系統(tǒng)的安全軟件測(cè)試研究[D];華東師范大學(xué);2017年

2 李中杰;基于全觀察者的多輸入輸出變遷系統(tǒng)拒絕測(cè)試研究[D];清華大學(xué);2004年

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

1 關(guān)愛(ài)華;基于輸入輸出理論的大學(xué)英語(yǔ)寫(xiě)作教學(xué)模式研究[D];哈爾濱師范大學(xué);2015年

2 馬慧舒;基于對(duì)稱(chēng)輸入輸出的三值ECL電路設(shè)計(jì)[D];浙江大學(xué);2006年

3 高紹全;高性能HSTL I/O Buffer研究與設(shè)計(jì)[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

4 胡軍;多變量系統(tǒng)干擾和輸入輸出同時(shí)解耦研究[D];天津大學(xué);2005年

5 李濤濤;基于ARM的嵌入式虛擬PLC系統(tǒng)的技術(shù)研究[D];廣東工業(yè)大學(xué);2013年

6 賈艷敏;FPGA中可編程輸入輸出緩沖器的設(shè)計(jì)[D];西安電子科技大學(xué);2013年

，

本文編號(hào)：1949792