形式手法入門 : ロジックによるソフトウェア設計 / / 中島震著

• Pubblicazione: 東京, : オーム社, 2012.4
• Descrizione fisica: オンライン資料1件
• Soggetto topico: ソフトウェア工学; システム設計
• Classificazione: 007.63; 007.61
• Nota di contenuto: 表紙 -- まえがき -- 目次 -- 1章 論理で考える -- 1.1 形式手法の概要 -- 1.1.1 高信頼化の総合技術 -- 1.1.2 複雑さと抽象化 -- 1.1.3 工学的な道具 -- 1.2 発展の経緯 -- 1.2.1 形式手法の変遷 -- 1.2.2 設計法と形式手法 -- 1.2.3 形式仕様言語の分類 -- 2章 指先で考える -- 2.1 Alloy入門 -- 2.1.1 Alloyの面白さ -- 2.1.2 Compositeパターン -- 2.1.3 抽象データの表現と解析 -- 2.1.4 機能仕様の表現と解析 -- 2.2 Alloyの基礎 -- 2.2.1 関係論理の考え方 -- 2.2.2 解析の方法 -- 2.2.3 有界モデル発見の限界 -- 2.3 Alloyとその周り -- 2.3.1 Alloyの歴史 -- 2.3.2 SATとSMT -- 3章 機能仕様を論理で考える -- 3.1 手続きとデータ構造 -- 3.1.1 状態ベースの仕様 -- 3.1.2 例題による形式手法の比較 -- 3.1.3 形式手法の比較 -- 3.1.4 2つの解釈 -- 3.2 正しさの基準 -- 3.2.1 正しさのいろいろ -- 3.2.2 型と型検査 -- 3.2.3 状態ベース仕様の証明条件 -- 4章 リファインメントを検査する -- 4.1 リファインメントとは -- 4.1.1 要求仕様とリファインメント -- 4.1.2 段階的な詳細化 -- 4.1.3 段階的な機能追加 -- 4.2 リファインメントの基礎 -- 4.2.1 2つの抽象レベル -- 4.2.2 模倣関係 -- 4.3 リファインメント検査 -- 4.3.1 リファインメントの証明条件 -- 4.3.2 Alloyとリファインメント -- 5章 オブジェクト指向デザインを検査する -- 5.1 クラス図とOCL -- 5.1.1 オブジェクト指向ソフトウェア開発とUML -- 5.1.2 静的な情報構造 -- 5.1.3 メソッドの機能振る舞い -- 5.2 モデリング言語OCL -- 5.2.1 OCLの変遷 -- 5.2.2 OCLの特徴 -- 5.2.3 3値論理 -- 5.3 オブジェクト指向概念と形式手法 -- 5.3.1 オブジェクト指向形式仕様言語 -- 5.3.2 オブジェクト指向デザインの形式化 -- 6章 振る舞い仕様を検査する -- 6.1 状態遷移システム -- 6.1.1 状態遷移マシン -- 6.1.2 述語論理による解釈 -- 6.1.3 UMLステート図 -- 6.2 時相的な振る舞いの自動解析 -- 6.2.1 時相論理 -- 6.2.2 有界モデル検査 -- 6.2.3 LTLの有界モデル検査 -- 6.2.4 ロジック・モデル検査 -- 6.2.5 イベント駆動スタイル -- 7章 プログラム検査を論理で考える -- 7.1 プログラムの意味 -- 7.1.1 Floyd/Hoareの方法 -- 7.1.2 プログラムの振る舞い解析の例 -- 7.1.3 VDMへの影響 -- 7.2 プログラムの検証 -- 7.2.1 ソフトウェア・モデル検査 -- 7.2.2 コントラクト -- 7.3 テストケースの自動生成 -- 7.3.1 ソフトウェアのテスト技術 -- 7.3.2 仕様に基づくテストケース自動生成 -- 7.3.3 モデル検査の利用 -- 付録 モデル規範形式手法の流れ -- A.1 概要 -- A.2 VDM -- A.3 Z記法とBメソッド -- A.4 集合ベースの方法 -- 索引 -- 奥付.
• Altri titoli varianti: 形式手法入門 : ロジックによるソフトウェア設計
• Titolo autorizzato: 形式手法入門
• ISBN: 4-274-83011-X
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Giapponese
• Record Nr.: 9910148969103321
• Lo trovi qui: Univ. Federico II