5H-06
形式手法と保証ケースによるコンポーネントの妥当性確認方式の提案
○山本椋太，山本修一郎（名大）
提案手法では，4つの形式的証拠を形式手法によって作成し，
GSN(Goal Structured Notation)における証拠として利用する．4つの形式的証拠 とは，(1)コンポーネントの入出力の検証，(2)コンポーネントの事前条件と事後条件の 検証，(3)コンポーネント間の相互作用の検証，(4)コンポーネント間の一貫性の検証のことである．本手法においては，これらの形式的証拠を形式手法のBおよびEvent-Bによって作成する方法を考えた．作成した形式的証拠をGSNから参照する．上記のように，形式手法と保証ケースを融合する方法を提案する．また，ケーススタディを作成し，実際の手法適用の流れを説明する．提案手法によって，保証ケースで重要となる客観的な証拠の作成が可能となった．
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会