組み込みソフトへの数理的アプローチ : 形式手法によるソフトウェアの仕様記述と検証
著者
書誌事項
組み込みソフトへの数理的アプローチ : 形式手法によるソフトウェアの仕様記述と検証
（Computer technology）
CQ出版, 2012.4
- タイトル読み
-
クミコミ ソフト エノ スウリテキ アプローチ : ケイシキ シュホウ ニヨル ソフトウェア ノ シヨウ キジュツ ト ケンショウ
大学図書館所蔵 全53件
この図書・雑誌をさがす
注記
参考文献: p240-243
内容説明・目次
内容説明
組み込みソフトウェアは年々巨大化し、従来の開発手法では品質が保証できなくなってきています。バグの発生は、ただちにシステムの障害に直結し、社会や人命に重大な損害を与えます。そこで登場した考え方として「形式手法（Ｆｏｒｍａｌ Ｍｅｔｈｏｄ）」があります。数学を基礎とし、プログラムの正しさを証明していこうという考えです。仕様を厳密に定義するための形式仕様記述、モデルの論理的な検証手法である形式検証について、ＬＴＳＡ、Ａｌｌｏｙ、ＣＢＭＣ、ＶＤＭなどの容易に入手できるツールを使いつつ学んでいきます。
目次
- 第１部 プログラムの基本、論理編（ソフトウェアの正しさをどう証明するか；仕様の形式化のはじめの一歩；推論の正しさの検証；前提が正しいとするとどんな結論を得られるのか—充足問題；真理表から場合分け表へ ほか）
- 第２部 組み込みの基本、ふるまい編（時間仕様の扱い；数理的アプローチによる開発；論理式のテスト；論理式の実験場を作る、全数チェックへの道；様相論理で変化を扱う ほか）
「BOOKデータベース」 より