Last Update 2020/11/24

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

藤倉 俊幸 著
B5変型判 248ページ
定価3,520円(税込)
JAN9784789838085
2012年4月15日発行
[品切れ重版未定2020.10.15] 組み込みソフトへの数理的アプローチ
大変恐縮ですが,こちらの商品は品切れ重版未定となりました.

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

目次

第1部 プログラムの基本,論理編

第1章 ソフトウェアの正しさをどう証明するか
第2章 仕様の形式化のはじめの一歩
第3章 推論の正しさの検証
第4章 前提が正しいとするとどんな結論を得られるのか―― 充足問題
第5章 真理表から場合分け表へ
第6章 AND-OR 木を形式化する
第7章 原因結果グラフ
第8章 組み合わせ問題とLTSA
第9章 組み合わせ問題で写像に親しむ
第10章 Alloy によるモデリング
第11章 要求のトレーサビリティとモデリング
第12章 プログラム検証とテスト
第13章 TDD(テスト駆動開発)におけるテスト
第14章 検証しながらプログラムを作るPDD
第15章 形式仕様記述は役に立つのか

第2部 組み込みの基本,ふるまい編

第16章 時間仕様の扱い
第17章 数理的アプローチによる開発
第18章 論理式のテスト
第19章 論理式の実験場を作る,全数チェックへの道
第20章 様相論理で変化を扱う
第21章 時相論理の導入: CTL とLTL
第22章 到達可能性と安全性を検証する
第23章 オーバーラップ制御用ステート・マシンの設計と検証