高信頼性ソフトウェアシステムの実現のためのモデル修正技術に関する研究

摘要

近年のソフトウェア開発は，システムの要求分析，設計をrn行った後にプログラムを実装するという手順で進められる．rn要求分析，設計工程では，状態遷移機械などのモデルを用いrnて，開発者が対象システムの振る舞いが記述されることが多rnい．開発したシステムが正しく動作し，高い信頼性を持つたrnめには，モデルが所望の性質や性質を正しく表現していなけrnればならない．そのため，モデルの正しさを形式的に検証すrnるモデル検査技術が数多く開発されている．