情報制御システムのモデル検査における反例分析支援ツールの開発  [in Japanese] An Analysis Support Tool of Counterexamples for Model-Checking of ICS  [in Japanese]

Search this Article

Author(s)

Abstract

情報制御システムを対象としたモデル検査は,安全性を確保する上で意味あるアプローチといえる.この際,任意の性質が満たされない実行系列 (反例) を得ることで不具合の原因特定に役立てることができる.しかし,反例を理解するには専門的な知識が必要となり,反例から振舞い仕様の問題箇所を特定するのは困難である.そこで本研究ではモデル検査ツールにおける反例分析支援のための可視化ツールを開発した.具体的な事例を適用しその結果,本ツールが問題箇所の特定において,有責な情報を提供できることがわかった.

Model checking for Information Control System is an effective approach in order to ensure safety. In this case, obtaining execution sequences not to satisfy properties(counterexample) is useful to find out cause of errors. However, we require expertise to understand the counterexample and it is difficult to identify error locations of behavior specification by the counterexample. Therefore, this study report about a visualizing tool which was developed to support analyzing counterexample on model checking tool SPIN. It found that developed tool can provide valuable information in identifying error locations.

Journal

  • IPSJ SIG Notes

    IPSJ SIG Notes 2014-SE-183(11), 1-8, 2014-03-12

    Information Processing Society of Japan (IPSJ)

Codes

  • NII Article ID (NAID)
    110009677118
  • NII NACSIS-CAT ID (NCID)
    AN10112981
  • Text Lang
    JPN
  • Data Source
    NII-ELS 
Page Top