形式手法 (MALACS) | 本位田研究室

研究内容概要 MALACS (Models And Languages for Correct Software)グループは，ソフトウェア開発に関連した形式手法技術を研究しています．仕様記述，検証，コード生成などが含まれます． モデル検査では，システムの状態をモデル化し不都合な状態遷移の発生を見つけることで，モデルの正しさを客観的に示します．正しいモデルに従ってソフトウェア開発を行うことで，開発の手戻りを軽減することができます. 形式手法の中でヘビーウェイトと言われている定理証明系は，モデル検査などで避けられない状態爆発の問題が発生しないた め注目を集めています．ソフトウェアの挙動を関数として定義し，その関数が満すべき性質を証明することで挙動の正しさを保証します．証明が与えられた関数 から実際に動作するプログラムコードを生成し，プログラム開発時のバグ発生を抑制することができます． 形式的仕