和書
- 形式手法の技術講座 (佐原伸/SRC)
- プログラム仕様記述論 (荒木啓次郎/オーム社)
- ソフトウェア科学基礎
- Bメソッドによる形式仕様記述
- SPINモデル検査―検証モデリング技法 (中島震/近代科学社)
- 形式手法モデル理論アプローチ (高原康彦 他/日科技連)
- ディペンダブルシステム
- SPINによる設計モデル検証 (吉岡信和 他/近代科学社 TopSE)
- 4日で学ぶモデル検査 (初級編) (産業技術総合研究所システム検証センター/NTS)
- NuSMV, SPIN; KNOPPIX CD-ROM付
- 組み込みソフトウェアの設計&検証
- ソフトウェア開発のモデル化技法 (J.フォッツジェラルド/P.G.ラーセン/岩波)
- 組み込みソフトウェア2007 モデルに基づく開発方法論の全て (日経BP)
洋書
- "Categolies and Computer Science" R F C Walters, Cambridge University Press
- 型理論の本を読むときに圏論の言葉が出てくることがある。そういった書籍の読解を助ける上でも良書。
- Modeling in Event-B: System and Software Engineering
- The SPIN Model Checker: Primer and Reference Manual
- Principles of the Spin Model Checker
- Principles of Model Checking
- Software Abstractions: Logic, Language, and Analysis (Daniel Jackson/MIT press)
- Systems and Software Verification: Model-Checking Techniques and Tools
- Model Checking
- Concurrency: State Models and Java Programs
- Validated Designs for Object-oriented System (J.Fitzgerald他/Springer)
- Verification of Object-Oriented Software, The KeY Approach (Bernhard Beckert他/Springer)
- Systems and Software Verification, Model-Checking Techniques and Tools (B.Berard他/Springer)
- モデル検査色々 (SMV, SPIN, DESIGN/CPN, UPPAAL, KRONOS, HYTECH)
最終更新:2010年04月12日 10:01