4. C言語へのフォーマルメソッドの適用(Part II:産業界への応用,<特集>フォーマルメソッドの新潮流)
スポンサーリンク
概要
- 論文の詳細を見る
ソフトウェアの信頼性を確保するための技術として形式手法が注目されている.我々は,C言語で記述されたソースコートから状態遷移モテルを自動的に作成し,有界モデル検査法によりソースコードに内在する不具合を引き起こすコードの検出や,表明によるプログラムの正しさを検鉦するツールであるVARVELの開発を行った.本稿では,本ツールが利用している要素技術や提供する機能,およびソフトウェア開発現場における適用事例について報告する.
- 2008-05-15
著者
関連論文
- 4. C言語へのフォーマルメソッドの適用(Part II:産業界への応用,フォーマルメソッドの新潮流)
- 形式手法によるC言語検証ツール「VARVEL」 (組込みソフトウエア・ソリユーシヨン特集) -- (組込みソフトウェア開発環境ソリューション)
- 高信頼ソフトウェア開発技法の実践的試み(システム設計のための形式手法の基礎と応用)