組み込みソフトへの数理的アプローチ : 形式手法によるソフトウェアの仕様記述と検証

書誌事項

組み込みソフトへの数理的アプローチ : 形式手法によるソフトウェアの仕様記述と検証

藤倉俊幸著

(Computer technology)

CQ出版, 2012.4

タイトル読み

クミコミ ソフト エノ スウリテキ アプローチ : ケイシキ シュホウ ニヨル ソフトウェア ノ シヨウ キジュツ ト ケンショウ

大学図書館所蔵 件 / 52

この図書・雑誌をさがす

注記

参考文献: p240-243

内容説明・目次

内容説明

組み込みソフトウェアは年々巨大化し、従来の開発手法では品質が保証できなくなってきています。バグの発生は、ただちにシステムの障害に直結し、社会や人命に重大な損害を与えます。そこで登場した考え方として「形式手法(Formal Method)」があります。数学を基礎とし、プログラムの正しさを証明していこうという考えです。仕様を厳密に定義するための形式仕様記述、モデルの論理的な検証手法である形式検証について、LTSA、Alloy、CBMC、VDMなどの容易に入手できるツールを使いつつ学んでいきます。

目次

  • 第1部 プログラムの基本、論理編(ソフトウェアの正しさをどう証明するか;仕様の形式化のはじめの一歩;推論の正しさの検証;前提が正しいとするとどんな結論を得られるのか—充足問題;真理表から場合分け表へ ほか)
  • 第2部 組み込みの基本、ふるまい編(時間仕様の扱い;数理的アプローチによる開発;論理式のテスト;論理式の実験場を作る、全数チェックへの道;様相論理で変化を扱う ほか)

「BOOKデータベース」 より

関連文献: 1件中  1-1を表示

詳細情報

ページトップへ