以AFSM為基礎的感測/驅動控制混合程式驗證

Abstract

在這篇論文中，我們發展一個方式將時序邏輯正規驗證法，應用在由Rodney Brooks所提出的增強化有限態機器(AFSM)所控制的自主性機器人上。 在這個方式中，我們使用了一些方法去簡化以AFSM為基礎的感應式機器控制系統(RRCS)的複雜度，讓以AFSM為基礎的RRCS之驗證能夠有可行性。這些被應用在驗證上的方法包括有：(1)狀態空間離散化――驗證一個在連續定義域上的系統是不可行的。因此，在建構一個以AFSM為基礎的RRCS之前，我們必須將系統及環境從連續定義域轉換到分散定義域。(2)外部函數――藉由OMocha所提供的外部函數，將系統中的內部狀態及運動學上的計算從驗證器中輸出至外部函數。(3) 去除掉不必要的檢驗部分――根據我們所要檢驗的行為特性，我們能夠將必定不會違背此特性的一些檢驗部分去除掉。 在運用了上述的這些方法後，結果中顯示，被OMocha檢驗的全部可到達狀態數目及檢驗時間都改善了很多。 在這篇論文中，我們將達成的一些成果列在下面： (1)用檢驗器檢驗以AFSM為基礎的RRCS之行為特性――在建構起以AFSM為基礎的RRCS後，我們用時序邏輯來描述”No_Collision”這個特性，並且證明了被此RRCS控制的機器人在二維空間中將永遠不會碰到障礙物。 (2)改善檢驗程序的效率――在藉由三個方法來縮短檢驗時間後，最佳的結果中顯示檢驗程序能夠在合理的時間內被完成。 根據這些成果，我們能夠證明將正規驗證應用在以AFSM為基礎的RRCS是可行的。

In this thesis, we develop a method to apply formal verification of Temporal Logic onto an autonomous robot system controlled by Rodney Brooks’ Augmented Finite State Machine model. This method uses some approaches to reduce the complexity of an AFSM-based reactive robot control system (RRCS), so that verification of AFSM-based RRCS can become applicable. These approaches applied onto verification include：(1) State Space Discretization――It is not feasible to verify a system on continuous space-time domain. Therefore, before constructing an AFSM-based RRCS we must transform the system and environment from continuous space domain to discrete space domain. (2) External function――By exporting internal states and kinematic computation of the robot from the model checker using the external function provided by OMocha temporal logic model checker. (3) Elimination of some checking cases――Based on the properties we want to check, we can eliminate some unnecessary checking cases which will never violate the properties. After using above-mentioned approaches, the results show that the number of all reachable states checked by OMocha and checking time improve greatly. In this thesis, we reach some accomplishments listed below： (1) Check the Behaviors of the AFSM-based RRCS by Model Checker――After constructing the AFSM-based RRCS, we describe the “No Collision” property by Temporal Logic, and prove that the robot controlled by the RRCS will never collide with obstacles in two-dimensional environment. (2) Improve the Performance of Checking Procedure――After reducing the checking time by the three approaches, the best results show that the checking procedure can be completed in reasonable time. According to the accomplishments, we can prove that it’s applicable to apply verification onto an AFSM-based RRCS.