本文選題：多形態(tài)時鐘 + 標號遷移系統(tǒng)　； 參考：《華東師范大學》2017年博士論文

【摘要】：缺乏系統(tǒng)的科學的測試體系是一直以來影響安全軟件測試可信度的根本問題。在現(xiàn)有的工程實踐中,測試是實驗性行為的認知和實施方案普遍存在,威脅著系統(tǒng)的安全性并且這一問題隨著安全軟件需求量的激增,職責范圍的外延,規(guī)模的擴大和復雜度的提高變得越來越嚴重。因此,構(gòu)造高效可信的安全測試方法和工具已經(jīng)成為安全軟件行業(yè)不可回避的挑戰(zhàn)。本文以構(gòu)建安全軟件的安全性測試理論框架及其應用為主要研究目標,針對安全軟件苛求質(zhì)量的實際需求,以形式化測試為基礎(chǔ),根據(jù)安全軟件的典型特征,從設(shè)計符合其特點的建模語言開始,構(gòu)建了統(tǒng)一安全性驗證和安全性測試的理論框架。該理論框架立足于研發(fā)安全軟件的全流程而非純粹測試的立場,在保證測試方法本身正確性的同時,設(shè)計了通過測試也可以證明軟件實現(xiàn)是安全的理論框架和相應的測試序列生成方法,主要貢獻體現(xiàn)在:1.定義了多形態(tài)時鐘時間模型,設(shè)計了多形態(tài)時鐘輸入輸出遷移系統(tǒng),給出了相應語法和語義的形式化定義,提出了將時間模型從系統(tǒng)行為模型中分離出來的安全軟件建模方法;2.提出了統(tǒng)一的安全性驗證與測試序列生成理論框架。該理論框架站在安全軟件全流程而非單一測試的角度,將對規(guī)約設(shè)計的安全性驗證與軟件實現(xiàn)的安全性測試融合在同一個理論框架中,證明了如果某個實現(xiàn)通過了基于滿足安全性屬性模型所生成的測試序列集合,那么該實現(xiàn)也滿足期望的安全性屬性的結(jié)論,并給出了相應的測試序列生成方法;3.構(gòu)建了多形態(tài)時鐘輸入輸出遷移系統(tǒng)的安全性測試方法,定義了多形態(tài)時鐘輸入輸出一致性關(guān)系,設(shè)計了相應的符號測試方法。并在此基礎(chǔ)上,為了滿足安全軟件防護能力測試的需求,進一步提出了采用規(guī)約變異的測試方法計算安全軟件的故障測試序列集合,定義了基于安全故障模型的變異算子,給出了基于弱變異思想的誘導規(guī)則,設(shè)計了k周期誘導算法。為了展示方法的可行性,本文以某實際車載列車自動防護軟件系統(tǒng)為例說明了基于多形態(tài)時鐘輸入輸出遷移系統(tǒng)的安全測試理論在安全軟件系統(tǒ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.
【學位授予單位】：華東師范大學
【學位級別】：博士
【學位授予年份】：2017
【分類號】：TP311.53

【相似文獻】

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

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

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

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

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

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

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

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

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

9 ;所見即所得——Adobe Photoshop 5.0應用色彩管理輸入輸出相一致[J];每周電腦報;1998年50期

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

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

1 楊振宇;陳宗基;;混合系統(tǒng)的一類混合輸入輸出自動機模型[A];1997年中國控制會議論文集[C];1997年

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：1949792