|
まず、故障をとらえた計算モデルを、プロセス代数・有限状態オートマトンの２つの枠組みで考察した。プロセス代数としては、ミルナーによるＣＣＳおよびパイ計算を中心に研究した。そして、従来モデルへの変換を与えることにより解析を行うことを試みた。この変換がモデルの意味を保存することを確認した。さらに、変換先の解析結果を変換元の性質として逆変換する方法についても研究した。
これらの成果を元に、バックエンドの推論システムにモデル検査システムを用いた検証システムを実装を試みた。実装については、ＵＰＰＡＡＬなどのモデル検査系に基づくものとなった。バックエンドからの解析結果をフロントエンドである故障をとらえた計算モデルに関する性質として表示することについて研究をすすめた。
さらに、プロセス代数ベースの計算モデルを定理証明システム上で形式化を行うことにより、形式的仕様記述の基盤を確立することを目指した。また、FMEAやFTAなどの信頼性工学の手法との統合についても検討した。
とりわけ、平成２９年度においては、これまでの研究成果を取りまとめの作業を行い、国際会議発表や学術雑誌掲載などに取り組んだ。また、これまでに研究した「故障をとらえるためのプロセス代数」や「故障を評価するための形式的検証ツールを用いた検証手法」などの個々の研究成果を総合的に評価し、その相互の関連について考察を進めた。
故障に関して形式的取り扱いをするための手法について一定の目途をつけることができた。
|
