Formal Verification of Logic Control Systems with Nondeterministic Behaviors

カテゴリ: 論文誌(論文単位)

グループ名: 【D】産業応用部門（英文）

発行日: 2013/11/01

タイトル(英語): Formal Verification of Logic Control Systems with Nondeterministic Behaviors

著者名: Saifulza Alwi (Department of Electrical and Computer Engineering Yokohama National University/Faculty of Electrical Engineering, Universiti Teknikal Malaysia Melaka (UTeM)), Yasutaka Fujimoto (Department of Electrical and Computer Engineering Yokohama Nat

著者名(英語): Saifulza Alwi (Department of Electrical and Computer Engineering Yokohama National University/Faculty of Electrical Engineering, Universiti Teknikal Malaysia Melaka (UTeM)), Yasutaka Fujimoto (Department of Electrical and Computer Engineering Yokohama National University)

キーワード: programmable logic controllers，formal methods，formal verification，model checking，timer function blocks

要約(英語): This paper describes a formal modeling and verification of an arm pick-and-place system, in which nondeterministic behaviors of the arm state condition and timer function blocks are applied. We design an appropriate PLC program using a ladder diagram (LD) for the arm pick-and-place operation and apply in it a situation where the arm may drop the product or material being gripped because of an external force. In addition, the timer function blocks are used with formalization of their finite-state logical properties. We use an actual model of the arm to verify that safe operations are established for normal product pick-and-place, as well as when the product has fallen. In addition, we perform arm model verifications for five important temporal properties using the NuSMV model checker. We present two types of experiments to validate the safety of the designed LD program. We also verify that the nondeterminism that appears as a result of the system behaviors can be formalized and used to represent logical assumptions for the properties that need to be verified.

本誌: IEEJ Journal of Industry Applications Vol.2 No.6 （2013） Special Issue on Technologies of Rotating Machinery

本誌掲載ページ: 306-314 p

原稿種別: 論文／英語

電子版へのリンク: https://www.jstage.jst.go.jp/article/ieejjia/2/6/2_306/_article/-char/ja/