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

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

• 要旨(「BOOK」データベースより）

  組み込みソフトウェアは年々巨大化し、従来の開発手法では品質が保証できなくなってきています。バグの発生は、ただちにシステムの障害に直結し、社会や人命に重大な損害を与えます。そこで登場した考え方として「形式手法（Ｆｏｒｍａｌ　Ｍｅｔｈｏｄ）」があります。数学を基礎とし、プログラムの正しさを証明していこうという考えです。仕様を厳密に定義するための形式仕様記述、モデルの論理的な検証手法である形式検証について、ＬＴＳＡ、Ａｌｌｏｙ、ＣＢＭＣ、ＶＤＭなどの容易に入手できるツールを使いつつ学んでいきます。

• 目次(「BOOK」データベースより）

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

• 著者紹介（「BOOK著者紹介情報」より）（本データはこの書籍が刊行された当時に掲載されていたものです）

  藤倉 俊幸(フジクラ トシユキ)
  エンジニアとして約３０年活動。博士（学術）はデータ・マイニングの一種で取得。２０１０年から株式会社エクスモーション勤務

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