「honto 本の通販ストア」サービス終了及び外部通販ストア連携開始のお知らせ
詳細はこちらをご確認ください。
このセットに含まれる商品
前へ戻る
- 対象はありません
次に進む
商品説明
離散状態をもつシステム、および離散状態と連続状態を併せもつハイブリッドシステムを形式的にモデル化するための手法を解説。モデルが与えられた仕様を満たしているかどうかを数理的に検証するための方法についても説明する。【「TRC MARC」の商品解説】
ソフトウェアが正しく設計されているかを保証するための手法として,システムを数学的に厳密なモデルで記述し,仕様が満たされているかどうかを数理的に調べる,「形式検証」が注目されている.
本書では,モデル検査に代表されるように,現実のシステムにも適用可能になってきた形式検証を理解し,使いこなすための理論的背景について解説する.
離散事象システム,実時間システム,ハイブリッドシステムなど,さまざまなシステムに対する形式的モデル化手法と,その解析方法が網羅された1冊.【商品解説】
目次
- ◆第Ⅰ部 システムのモデル化
- 第1章 システムの概念
- 第2章 オートマトンと形式言語
- 第3章 ペトリネット
- 第4章 プロセス代数
- ◆第Ⅱ部 性質・ふるまいの記述
- 第5章 時相論理によるシステムの性質の記述
- 第6章 遷移システム・ラベル付き遷移システム
著者紹介
平石 邦彦
- 略歴
- 〈平石邦彦〉東京工業大学理工学研究科制御工学専攻修了。北陸先端科学技術大学院大学情報科学研究科教授。同大学情報社会基盤研究センター長。工学博士。
関連キーワード
あわせて読みたい本
前へ戻る
- 対象はありません
次に進む
この著者・アーティストの他の商品
前へ戻る
- 対象はありません
次に進む