DSW2015 Poster

人的欠陥に対する耐性解析のモデル検証的アプローチ（ポスター）

永藤直行, 渡部卓雄
第13回ディペンダブルシステムワークショップ(DSW 2015), Dec. 16-17, 2015.

概要

人的欠陥に対する手順の堅牢性解析についてモデル検証的アプローチを提案する． 工場，病院，飛行機など様々なところで手順が定義・利用され，人間が実行する． 人によって実行される手順には人的欠陥に伴うエラーを発見・回復するためのタスクが含まれている． 発見・回復のタスクが期待通りに機能するかどうかはその手順の信頼性を保つ上で重要である． 信頼性を確保するため，人的欠陥を埋め込み検査する手法を利用する． 人的欠陥は Swain の Discrete Action Classification にしたがって埋め込まれる． 我々の手法では，人的欠陥を埋め込んだモデルを対象にエラー状態に至る経路を探索するためにモデル検査の手法を利用する． 手順はプロセス代数に基づいてモデル化し，モデルが充たすべき性質はその手順の目的を表した論理式であり，論理式は時相論理の式として与えられる．