完整後設資料紀錄
DC 欄位語言
dc.contributor.author龔哲正en_US
dc.contributor.author邵家健en_US
dc.date.accessioned2014-12-12T02:55:07Z-
dc.date.available2014-12-12T02:55:07Z-
dc.date.issued2005en_US
dc.identifier.urihttp://140.113.39.130/cdrfb3/record/nctu/#GT009317542en_US
dc.identifier.urihttp://hdl.handle.net/11536/78752-
dc.description.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是可行的。zh_TW
dc.description.abstractIn 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.en_US
dc.language.isozh_TWen_US
dc.subject正規驗証zh_TW
dc.subject強化有限態機器zh_TW
dc.subject機器人控制系統zh_TW
dc.subjectformal verificationen_US
dc.subjectAFSMen_US
dc.subjectrobot control systemen_US
dc.title以AFSM為基礎的感測/驅動控制混合程式驗證zh_TW
dc.titleHybrid Program Verification for AFSM-based Sensory-Motor Controlen_US
dc.typeThesisen_US
dc.contributor.department資訊科學與工程研究所zh_TW
顯示於類別:畢業論文


文件中的檔案:

  1. 754202.pdf

若為 zip 檔案,請下載檔案解壓縮後,用瀏覽器開啟資料夾中的 index.html 瀏覽全文。