| 研究生: |
許嘉豪 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.
[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公開