形式手法は、システム構築の首尾一貫性に関する証明可能性や、実現するシステムの機能安全性の観点より注目されてい る。我々は、本校情報工学科の実験で採用している簡易 CPU モデルを形式手法 B-Method により記述した。 B-Method による記述を通じて、開発ツールにおけるモデルの記述と論理証明、検証ツールにおける認証とアニメーション （シミュレーションに相当）に成功したのと同時に、モデルの記述の証明、認証等に際しての困難性に関する知見を得た。