基於線性時序邏輯之安卓系統程式的整合式測試評估框架

Abstract

由於行動裝置技術的快速蓬勃發展，行動裝置應用程式的重要性以及數量都呈現爆炸性發展的趨勢。如何去驗證以及維護這些應用程式的品質已經是現今一個非常重大的問題，因此，有效率且自動化的測試是非常必要的。 在軟體測試中，線性時序邏輯是一個非常適合用來描述這些行動裝置應用程式行為的語言，但對於普通使用者而言，它卻是難以理解的。 在這篇論文中，我們呈現了一個使用線性時序邏輯特徵公式來測試安卓系統上應用程式的一個框架。這個框架包含了一個圖形介面工具，可以幫助使用者自動地或手動地創建線性時序邏輯公式來描述待測程式的行為，另外還包含了一個測試評估程序，可以用來評估測試結果數據是否符合我們所定義的線性時序邏輯公式特徵。我們的目標是提供一個專業的測試方式，以及在測試評估中獲得更高的準確率。

Along with the rapid development of mobile techniques, the importance and quantity of mobile device applications takes on a trend of explosive increase. How to verify and maintain the quality of these applications becomes a huge problem today, so an efficient automated testing is necessary. LTL (Linear temporal logic) is a well-suited language to describe the behaviors of mobile device applications for software testing. But it’s also incomprehensible to most of common people. In this thesis, we present a framework to perform the testing for Android applications with LTL properties. The framework contains a tool with GUI to help users to construct their own LTL formulas automatically or manually (depending on user’s choice) to describe the specification of the SUT (system under test), and a trace evaluator to determine whether the traces of the SUT satisfy the given LTL property or not. Our goal is offering more professional testing method and getting higher accuracy in test evaluation.