簡易檢索 / 詳目顯示

研究生: 許嘉豪
Hsu, Chia-Hao
論文名稱: 針對符合國際標準IEC61499之功能塊進行自動模型轉換與正規驗證
Automatic Model Transformation and Formal Verification for Function Block of International Standard IEC61499
指導教授: 陳盈如
Chen, Yean-Ru
學位類別: 碩士
Master
系所名稱: 電機資訊學院 - 電機工程學系
Department of Electrical Engineering
論文出版年: 2019
畢業學年度: 108
語文別: 中文
論文頁數: 113
中文關鍵詞: IEC61499 標準模型驗證模型組合模型轉換
外文關鍵詞: IEC61499 standard, Model checking, Model composition, Model transformation
相關次數: 點閱:70下載:1
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報
  • IEC61499標準主要內容為描述分散式控制系統結構與行為,提供了在系統層級的設計語言,為分散式的系統提供一個規範。IEC61499標準在設計系統上,主要是先進行整體系統的設計,然後將設計好的功能塊網路,分散給不同的裝置去做運算,各個功能塊藉由標準制定的接口傳輸資料與控制流,以達成分散式控制系統的行為。

    IEC61499標準的功能塊,在控制流的設計上,會採用一種類似於有限狀態機的執行控制圖(Execution Control Chart)來描述功能塊的行為,而其實在IEC61499標準中,也有設計了運作狀態機(Operation State Machine),來描述功能塊的運作。因此在真正的功能塊運作上,其實是需要同時考慮執行控制圖與運作狀態機之間的互動行為。

    本篇論文提出一個自動將功能塊模型轉換成有限狀態機模型的方法,主要包含三個演算法,第一個演算法描述我們如何將執行控制圖與運作狀態機組合成完整表達功能塊控制行為的模型,第二個演算法會將使用者輸入的行為做組合,用一個模型完整表達在狀態內所需執行的運算行為,第三個演算法再將以上演算法輸出的模型做整合,獲得完整表達功能塊運作的有限狀態機模型。最後將轉換後的有限狀態機輸入至模型驗證器進行正規驗證。

    The main content of the IEC61499 standard is to describe the structure and behavior of decentralized control systems. In the design system, the IEC61499 standard mainly designs the overall system first, and then distributes the designed function block network to different devices for calculation.

    The function block of the IEC61499 standard, in the design of the control flow, uses an execution control chart to describe the behavior of the function block. In fact, in the IEC61499 standard, the operational state machine is also designed. Therefore, in the operation of the real function block, it is actually necessary to consider the interaction between the execution control chart and the operational state machine.

    This paper proposes a method for automatically transforming a functional block model into a finite state machine model. It mainly consists of three algorithms. The first algorithm describes how we compose the execution control chart with the operational state machine to fully express the functional block control behavior. The model, the second algorithm composes the actions input model by the user, and uses a model to fully express the computational behavior that needs to be performed in the state. The third algorithm then integrates the model output from the above algorithm to obtain the completeness. A finite state machine model that expresses the execution of a function block. Finally, the transformed finite state machine is input to the model checker for formal verification.

    摘要 i Abstract ii 英文延伸摘要 iii 誌謝 vi 目錄 vii 圖片 viii 第一章緒論1 1.1 IEC61499 標準 1 1.2 IEC61499 標準分散式系統設計 2 1.3 各種功能塊 3 1.4 基本功能塊內部介紹 4 1.5 功能塊執行語意 6 1.6 模型驗證 7 1.7 研究動機 9 1.8 論文貢獻 10 1.9 論文組織 10 第二章文獻探討12 2.1 功能塊控制行為與額外資訊 12 2.2 IEC61499 系統驗證 15 2.3 有限狀態機 17 第三章研究方法19 3.1 研究方法介紹 19 3.2 基本功能塊介紹 20 3.2.1 基本功能塊介面 20 3.2.2 執行控制圖與演算法 21 3.2.3 運作狀態機 25 3.2.4 ECC 與OSM 的搭配與互動 27 3.2.5 OSM 的重要性 28 3.3 驗證工作流程 29 3.4 基本功能塊定義 31 3.5 分散式系統輸入模型 38 3.5.1 子行為有限狀態機模型 41 3.6 功能塊控制模型 45 3.6.1 功能塊控制模型定義 46 3.6.2 模型組合演算法 49 3.6.3 功能塊控制模型初始狀態 52 3.6.4 功能塊控制模型例子 53 3.7 完整運算行為模型 56 3.8 事件與資料訊號處理 58 3.8.1 輸入與輸出事件訊號處理 58 3.8.2 資料訊號處理 60 3.9 有限狀態機模型 61 3.10 有限狀態機例子 64 3.11 檢查行為等價(behavioral equivalence) 65 3.11.1 功能塊執行模型 65 3.11.2 Bisimulation 66 3.11.3 證明過程 67 3.12 事件資料關聯性(Event/Data Association) 74 第四章實驗結果 77 4.1 紅綠燈控制系統 77 4.2 環境溫度控制系統 91 4.3 引擎速度控制系統 100 第五章結論 112 參考文獻 113

    [1] International Standard IEC61499-1: Function blocks Part1: Architecture, 1st ed. International
    Electrotechnical Commission, 2005.
    [2] Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal
    —a tool suite for automatic verification of real-time systems. In International hybrid
    systems workshop, pages 232–243. Springer, 1995.
    [3] Frédéric Boussinot and Robert De Simone. The esterel language. Proceedings of the
    IEEE, 79(9):1293–1304, 1991.
    [4] Tsun S. Chow. Testing software design modeled by finite-state machines. IEEE transactions
    on software engineering, (3):178–187, 1978.
    [5] JAMES H Christensen, THOMAS Strasser, ANTONIO Valentini, VALERIY Vyatkin,
    and ALOIS Zoitl. The iec 61499 function block standard: Overview of the second
    edition. ISA autom. Week, 6:6–7, 2012.
    [6] Victor Dubinin and Valeriy Vyatkin. Towards a formal semantic model of iec 61499
    function blocks. In 2006 4th IEEE International Conference on Industrial Informatics,
    pages 6–11. IEEE, 2006.
    [7] Bernd Glatz, Fionn Cleary, Martin Horauer, Harald Schuster, and Peter Balog. Complementing
    testing of iec61499 function blocks with model-checking. In 2016 12th
    IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications
    (MESA), pages 1–7. IEEE, 2016.
    [8] Inc. HOLOBLOC. FBDK 2.6 - The Function Block Development Kit.
    http://ftp.holobloc.com/fbdk2/index.htm/.
    [9] Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, and Jin Song Dong. Automatic
    generation of provably correct embedded systems. In International Conference on Formal
    Engineering Methods, pages 214–229. Springer, 2012.
    [10] Valeriy Vyatkin. The iec 61499 standard and its semantics. IEEE Industrial Electronics
    Magazine, 3(4):40–48, 2009.
    [11] Valeriy Vyatkin, Victor Dubinin, Carlo Veber, and Luca Ferrarini. Alternatives for execution
    semantics of iec61499. In 2007 5th IEEE International Conference on Industrial
    Informatics, volume 2, pages 1151–1156. IEEE, 2007.
    [12] Li Hsien Yoong and Partha S Roop. Verifying iec 61499 function blocks using esterel.
    IEEE Embedded systems letters, 2(1):1–4, 2010.

    無法下載圖示 校內:2024-11-04公開
    校外:不公開
    電子論文尚未授權公開,紙本請查館藏目錄
    QR CODE