LTLで記述されるマニュアルに対するオートメーションサプライズの検出 Detection of Automation Surprises for a Manual Modeled by Linear-Time Temporal Logic

この論文にアクセスする

この論文をさがす

著者

抄録

In a human-machine system, an interface displays an abstracted state of the machine. The abstracted state may differ from that anticipated by a user. Such a phenomenon is called an automation surprise and may cause a serious human error. In this paper, we assume that the user operates the machine according to a manual which is modeled by LTL (Linear-Time Temporal Logic). We propose a formal method for detection of three automation surprises and livelocks due to the manual. First, we transform the LTL representation of the manual into a transition system. Next, we propose a composite model derived from the transition system and a machine model, which describes concurrent behavior of the machine and the user. Finally, solving a reachability problem and searching strongly-connected components for the composite model, both the automation surprises and live lock can be detected formally.

収録刊行物

  • システム制御情報学会論文誌  

    システム制御情報学会論文誌 19(9), 350-357, 2006-09-15 

    一般社団法人 システム制御情報学会

参考文献:  14件

参考文献を見るにはログインが必要です。ユーザIDをお持ちでない方は新規登録してください。

被引用文献:  1件

被引用文献を見るにはログインが必要です。ユーザIDをお持ちでない方は新規登録してください。

各種コード

  • NII論文ID(NAID)
    10018416683
  • NII書誌ID(NCID)
    AN1013280X
  • 本文言語コード
    JPN
  • 資料種別
    ART
  • ISSN
    13425668
  • NDL 記事登録ID
    8055714
  • NDL 雑誌分類
    ZM11(科学技術--科学技術一般--制御工学)
  • NDL 請求記号
    Z14-195
  • データ提供元
    CJP書誌  CJP引用  NDL  J-STAGE 
ページトップへ