指導教授：王凡臺灣大學：電機工程學研究所陳品亘Chen, Pin-HsiuanPin-HsiuanChen2014-11-282018-07-062014-11-282018-07-062014http://ntur.lib.ntu.edu.tw//handle/246246/262881在行動運算裝置及雲端服務上的軟體發展呈現了一範式轉移。在這新的轉變下，測試者有可能需要時常想辦法處理沒有程式碼和最新說明文件的待測物。而在業界裡，最花測試工程師心力的，莫過於撰寫待測系統的測資和測試腳本。在這篇論文中，我們將介紹一自動化產生測資的架構，包含建立待測應用程式的運行記錄、建立模型和依據模型及線性時序邏輯來產生測資。執行測資並檢驗其是否合格。只要在一條測試結果為失敗的運行記錄中，所有動作都在測試時被觀察到，則我們所提出的測試流程必能產生一對應到該失敗結果的測資。實做上，我們將此架構建置成針對 Android 手機應用程式並實驗及提出報告。Software development of mobile computing and cloud services presents a paradigm shift. In this new paradigm, we may often need to deal with system under test (SUT) without source code and up-to-date documentation of the SUT. And when it comes to software testing in the industry, engineers often spend lots of effort to produce test cases themselves, writing script or manipulating SUT. Here we introduce a framework of automatic test case generation procedure that creating SUT trace, building the model of an SUT out of execution traces, and generating test cases according to the built model with specifications in Linear-time Temporal Logic (LTL). Then executing the test cases to check the SUT and examining the validation of test cases. As long as all transitions in a fail trace have been observed in the test session, then our procedure will eventually generate a test case that corresponds to the fail trace. We implement and report experiments on Android mobile applications.口試委員會審定書 # 誌謝 1 中文摘要 2 ABSTRACT 3 CONTENTS 4 Chapter 1 Introduction 6 1.1 Background 6 1.2 Motivation 6 1.3 Purpose 7 1.4 Theoretical model and LTL 7 1.5 Experiment design 10 1.6 System function 11 1.7 Organization 13 Chapter 2 Running example 14 2.1 Testing responsiveness with a model-checker 15 2.2 Testing via building the model 15 2.3 Enumerating counter-examples 17 2.4 Handling nondeterminism 18 Chapter 3 Related work 20 Chapter 4 Preliminary 22 4.1 Traces 22 4.2 Models 23 4.3 Linear-time Temporal Logic (LTL) 24 4.4 LTL model-checking and counterexamples 25 4.5 Android OS and SDK 26 Chapter 5 Dynamic test case generation procedure 28 5.1 High-level description of our testing procedure 28 5.2 Preprocessing 29 5.3 How to check that a trace violates an LTL property 30 5.4 How to guarantee generating new counter-examples 31 5.5 The completeness of our testing procedure 32 Chapter 6 Implementation 34 6.1 Android ripping 34 6.2 Web application as a testing service 34 6.3 Modeling 36 6.4 Use case 36 Chapter 7 Experiments 38 7.1 Benchmarks 39 7.2 Experiment platform 41 7.3 Experiment 1 41 7.4 Experiment 2 43 7.5 Experiment 3 46 7.6 Trace collection 47 Chapter 8 Concluding remarks 49 REFERENCE 51823742 bytesapplication/pdf論文公開時間：2016/08/17論文使用權限：同意有償授權(權利金給回饋學校)軟體測試Android應用程式測試線性時序邏輯模型檢查thesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/262881/1/ntu-103-R01921087-1.pdf