書籍

和書

• 形式手法の技術講座 (佐原伸/SRC)
  • VDM++
• プログラム仕様記述論 (荒木啓次郎/オーム社)
  • VDM-SL, Z
• ソフトウェア科学基礎
• Bメソッドによる形式仕様記述
• SPINモデル検査―検証モデリング技法 (中島震/近代科学社)
  • SPIN
• 形式手法モデル理論アプローチ (高原康彦 他/日科技連)
  • MTA-SDK
• ディペンダブルシステム
• SPINによる設計モデル検証 (吉岡信和 他/近代科学社 TopSE)
  • SPIN
• 4日で学ぶモデル検査 (初級編) (産業技術総合研究所システム検証センター/NTS)
  • NuSMV, SPIN; KNOPPIX CD-ROM付
• 組み込みソフトウェアの設計&検証
• ソフトウェア開発のモデル化技法 (J.フォッツジェラルド/P.G.ラーセン/岩波)
  • VDM-SL
• 組み込みソフトウェア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)
  • Alloy
• 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)
  • VDM++
• Verification of Object-Oriented Software, The KeY Approach (Bernhard Beckert他/Springer)
  • KeY (JML)
• Systems and Software Verification, Model-Checking Techniques and Tools (B.Berard他/Springer)
  • モデル検査色々 (SMV, SPIN, DESIGN/CPN, UPPAAL, KRONOS, HYTECH)