フォルトツリー解析からOTS/CafeOBJによるシステムの形式仕様記述および検証へ

DOI
  • 向 剣文
    北陸先端科学技術大学院大学情報科学研究科
  • 緒方 和博
    北陸日本電気ソフトウェア株式会社 北陸先端科学技術大学院大学安心電子社会研究センター
  • 孔 維強
    北陸先端科学技術大学院大学情報科学研究科
  • 二木 厚吉
    北陸先端科学技術大学院大学情報科学研究科

書誌事項

タイトル別名
  • From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ

抄録

The aim of this work is to provide a common semantic model for safety analysis and requirements formulation and verification. This paper investigates how the results of one safety analysis technique, fault trees, are interpreted as safety requirements and transformed into formal system specifications written in CafeOBJ, a formal algebraic language. We propose a common semantic model for both formal fault tree analysis and formal system specification by using observational transition systems (OTSs). The method not only can solve the informal problem of traditional fault trees, but more importantly, makes it possible to use the results of fault tree analysis directly, when specifying and verifying the system.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1390282679714314880
  • NII論文ID
    130004549057
  • DOI
    10.11309/jssst.23.3_134
  • ISSN
    02896540
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ