CQ出版WebShop,書籍案内へようこそ

CQ出版トップページへWebShop書籍・雑誌総合案内会員登録・変更ご利用案内

買い物カゴを見る

WebShop書籍・雑誌総合案内COMPUTER TECHNOLOGYシリーズ>組み込みソフトへの数理的アプローチ

書籍・雑誌総合案内
WebShop内検索(googleで本サイトを検索:別ウィンドウ)

COMPUTER TECHNOLOGYシリーズ

形式手法によるソフトウェアの仕様記述と検証

組み込みソフトへの数理的アプローチ

B5変型判 248ページ
定価3,520円(税込)
JANコード:JAN9784789838085
2012年4月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章 オーバーラップ制御用ステート・マシンの設計と検証

関連商品

ページトップへ

書籍・雑誌総合案内

Copyright(C) 2019 CQ Publishing Co.,Ltd.All rights reserved

会社案内求人情報プライバシ・ポリシお問い合わせ