代数仕様によるプラント機器保護論理の記述と検証

概要

論文の詳細を見る
プラント機器保護論理とは,異常発生時に対象機器を安全に停止させることを目的としたプラント機器保護装置で実現される安全保護のための論理である.保護論理はその役割から高い信頼性を必要とするため,形式的手法を用いた厳密な検証が一つの有望な手段と考えられる.我々は,形式仕様,とりわけ代数仕様に重点を置いて研究を続けている.代数仕様は,定理証明手続きを用いて仕様の自動検証ができることを特長とする.しかし,保護論理の検証にどのように代数仕様を適用するかは自明な問題ではない.そこで,プラント機器保護論理を対象とした代数仕様による記述・検証方式を提案する.設計図に用いられる部品を代数仕様で関数定義し,設計を抽象データ型上の関数とみなす.一方,要求をブール型の等式として記述する.記述された設計と要求から定理を整形し,定理証明手続きにかける.こうして設計が要求を満たすことを検証する.さらに,提案する方式に基づき現実の保護論理を対象に検証実験を行った.本稿では,この記述・検証方式と,検証実験の結果明らかになった実適用上の問題点とその解決について述べる.
一般社団法人情報処理学会の論文
1995-02-15