ソフトウェア開発方法論 北陸先端科学技術大学院大学 片山卓也 平成13年3月7日

目標 科学的方法論に基づく実用的ソフトウェア開発方法論の確立 科学的・理論的研究にもとづいたパラダイムや方法論によって現実のソフトウェア開発問題を解決する 理論のためだけの研究は行わない 現実問題の複雑性、規模を考えたアプローチ Toy problemsだけに適用可能な手法はとらない 平成13年3月7日

背景 現代社会を支える大規模、高度ソフトウェアの開発・保守の必要性 ソフトウェア開発方法論の実務 ソフトウェア開発のための理論 オブジェクト指向方法論、ソフトウェアプロセス、開発環境 ソフトウェア開発のための理論 形式的仕様記述、意味論、検証法 ソフトウェア開発の実務と理論の乖離 理論的成果が現実のソフトウェア開発に生かされていない 新しいソフトウェアに対する需要 モーバイル、分散協調 平成13年3月7日

サブプロジェクト 発展的ソフトウェア開発方法論（北陸先端大：片山） ソフトウェア開発アルゴリズム（早稲田：二村） 形式的オブジェクト指向開発方法論、発展的ソフトウェア開発原理・方式、フォールトトレラント ソフトウェア開発方法論 ソフトウェア開発アルゴリズム（早稲田：二村） 一般部分計算（ＧＰＣ)にもとづくプログラム最適化、プログラム性能・信頼性評価 ソフトウェア開発における形式化技術と環境（東工大：米崎） 形式論理に基づく平行・分散システムの仕様記述、定理証明技術による仕様検証および環境 開放性をもつ並行・分散ソフトウェア記述系(東大：米澤) モバイルプログラミング言語の設計と実装 平成13年3月7日

北陸先端科学技術大学院大学 要求分析、ソフトウェア発展 問題 Ｐ 実世界 Ｗ 東京大学 仕様書 モーバイル言語、 安全性 東京工業大学 形式的オブジェクト指向方法論 ソフトウェア発展方式、メカニズム 実世界 Ｗ 東京大学 仕様書 モーバイル言語、 安全性 Spec Item 1：pop(push(X,s))=X Spec Item 2：∀x1,x2∃z1,z2. { x1,x2≧0⊃x1=x2*z1+z2 Λ 0≦z2＜x2} 東京工業大学 仕様検証 設計と実装 形式論理による仕様記述 定理証明 早稲田大学 プログラム生成・最適化、評価 一般化部分計算、評価システム自動生成 平成13年3月7日

研究成果 代表的研究成果 形式的オブジェクト指向分析支援環境F-Developer、リアクティブモデルObTS実行環境、ソフトウェア発展のための理論体系(片山グループ) GPCによるプログラム自動超高速化システムWSDFU、テストデータ自動生成システム、計算量自動評価器(二村グループ) 時間論理によるリアクティブシステム仕様記述記述のための種々の論理体系、時間論理証明システムT3(米崎グループ) 移動コード技術に基づく安全なソフトウェア構築ため言語の設計と実装、次世代ネットワークソフトウェア配信システム(米沢グループ) 平成13年3月7日

開催したワークショップ、国際会議（11件） International Workshop on Principles of Software Evolution, （Kyoto, April,1998） ---（Fukuoka,July,1999） International Symposium on Principles of Software Evolution, Kanazawa, Nov. 2000 Waseda Partial Evaluation and Program Transformation Day, Nov.15, Tokyo,1999 プログラム変換と記号・数式処理シンポジウム、Nov.1999, 京都 Colloquium on Attribute Grammar and Program Optimization, Tokyo, July, 2000 International Software Engineering Symposium, China, March, 2001 International Workshop on Timed System, Kyoto, March，1999 International Workshop on Software Specification and Design, Toba, May, 1998 Workshop on Foundations for Secure/Survival Systems and Networks, Tokyo, 2001 International Workshop on Mobile Objects/Code and Security, Tokyo, Oct.2000 平成13年3月7日

ランダムデータジェネレータ生成方式およぶそのプログラム 連結グラフの生成方式およびそのプログラム 出願準備中2件 新聞報道 査読つき論文総数　１７８ 招待講演、論文　　　２１件 特許 　　(二村グループ) ランダムデータジェネレータ生成方式およぶそのプログラム 連結グラフの生成方式およびそのプログラム 出願準備中2件 新聞報道 　　（二村グループ）　5件 平成13年3月7日

公開ソフトウェア リアクティブシステム設計支援システムObTS 形式的オブジェクト指向分析支援システムF-Developer ランダムデータサーバ　RDS T(n)ソルバー プログラム高速化システムWSDFU T3エンジン、ビューワ、プリコンパイラ デザインパターンにもとづクラス図作成支援システム CTAGシステム PF-Webシステム CATシステム Stack Threads/MP Distributed GC JavaGo MIC 平成13年3月7日

発展的ソフトウェア開発方法論 （片山グループ） 研究内容 発展的にソフトウェアを開発するための原理とそのためのモデル、方法論 発展的ソフトウェア開発原理・方式 発展ドメイン理論によるソフトウェア発展原理 抽象解釈原理にもとづく発展的ソフトウェア開発法 形式的オブジェクト指向方法論 形式的分析モデル構築・検証システム リアクティブシステム構築システム 平成13年3月7日

発展的ソフトウェア開発原理・方式 発展ドメイン理論によるソフトウェア発展原理 抽象解釈原理にもとづく発展的ソフトウェア開発法 発展ドメイン： 許容可能な仕様やプログラムの「変化」を表す順序構造 合理的な発展を許容する開発プロセス： 発展ドメイン間の準同型写像 抽象解釈原理にもとづく発展的ソフトウェア開発法 段階的詳細化法 詳細化の初期の段階から抽象的に動かす データの抽象化：　 関数型プログラム イベントの抽象化： オブジェクトの振る舞いの段階的構築 平成13年3月7日

形式的オブジェクト指向方法論 オブジェクト指向方法論 ソフトウェア設計の最も有効かつ自然な設計･開発方法論 現在のオブジェクト指向開発方法論 形式性が低く有効な計算機支援が困難。 分析から実装までの一貫した方法論が存在しない。 平成13年3月7日

形式的オブジェクト指向方法論 形式的アプローチ 仕様やモデルを数学的対象としてとらえる。 オブジェクト指向方法論への形式的アプローチ 「形式的方法論」のオブジェクト指向化 オブジェクト指向 Ｚ、代数的アプローチ、ＶＤＭ、･･･ 現実のオブジェクト指向方法論の実際とは方向性が異なる。 現実に行われているオブジェクト指向方法論の形式的アプローチが必要。 平成13年3月7日

形式的オブジェクト指向方法論 目標： 形式的手法にもとづく一貫した方法論の展開 形式的モデル記述体系 分析モデル間の整合性、統合モデルの構成 目標：　形式的手法にもとづく一貫した方法論の展開 形式的モデル記述体系 複数の観点からのモデル化 オブジェクトモデル、動的モデル、… UML：9モデル 分析モデル間の整合性、統合モデルの構成 分析モデルの適切性・一貫性の検証 統合モデルのプロトタイプ実行 定理証明技術による検証 統合モデルからソフトウェアアーキテクチャへの変換 ソフトウェアアーキテクチャ + 実装モデル => 実装 平成13年3月7日

形式的オブジェクト指向方法論 通常のオブジェクト指向方法論 非形式的分析モデル(図形+自然言語) 要求 分析 設計 実装 クラスモデル 要求 分析 動的モデル 設計 実装 …モデル 設計・実装段階でのモデル統合 (設計・実装者の頭の中) 平成13年3月7日

形式的オブジェクト指向方法論 本形式的方法論 要求 分析 形式的モデル 実行可能モデル 定理証明技術の利用 モデル統合 統合モデル クラスモデル 実行可能モデル 要求 分析 動的モデル モデル統合 統合モデル …モデル プロトタイプ 実行 一貫性検証 ソフトウェア アーキテクチャ 決定 ソフトウエア 生成・実装 ソフトウェア 定理証明技術の利用 実装モデル 平成13年3月7日

形式的オブジェクト指向方法論（研究成果） 形式的モデルF-Model（関数モデル） クラスモデル 統合写像 要求 分析 動的モデル モデル統合 統合モデル 機能モデル リアクティブシステム モデルObTS モデル構築システム F-Developer （エディター、プロトタイパー、検証系） プロトタイプ 実行 一貫性検証 ソフトウェア アーキテクチャ 決定 ソフトウエア 生成・実装 ソフトウェア 不変制約検証公理系 データフロー検証公理系 定理証明系HOLによる実装 スレッドモデルへの変換 SESモデル 実装モデル 平成13年3月7日

形式的オブジェクト指向方法論 オブジェクト指向分析への形式性の導入では最も先進的 分析モデルの統合、不変制約のための公理系 分析過程への本格的定理証明技術の利用 概念の再利用などが可能な高階論理 標準言語UML：制約記述言語OCLによる不変制約記述 MIT：有限領域についての「軽い」整合性検証 ＮＡＳＡ、UCI　：完成された状態図 一般ソフトウェア技術者が使える段階には、更なら研究が必要 OCL　=>　SQL　変換 分析モデルの実行 通常は、分析モデルは実行出来るほど形式性が高くない ObTSモデルは、Statechartモデルの最も自然なオブジェクト指向拡張 公開システムとして分析環境を構築 平成13年3月7日

統合分析支援環境 F-Developer 1. 形式的分析モデルF-Modelに基づいたモデル構築 Model Builder 2. 構築した分析モデルを、関数型言語処理系SML上で 　　　プロトタイプ実行 F-Prototyper 3. 構築した分析モデルを、定理証明系HOLを用いて検証 F-Verifier Model Builder 独立なモデル構築 基本クラスモデル 統合写像の入力 基本ステートチャートモデル 平成13年3月7日

プロトタイプ実行環境 F-Prototyper 1. F-Prototyperでは構築した分析モデルのプロトタイプ実行を 　　関数型言語処理系SML上で行う。 2. プロトタイプ実行に必要な実行系を自動生成 3. オブジェクトが持つ属性やメソッドの計算をSMLの関数で与える 実行系自動生成器＆ SMLインタプリタ 分析モデルにSMLの関数を割り当て アニメーションで動作を確認 実行スクリプトエディタで、実行系列を定義 (* INSTANTIATE OBJECT*) Class_IncrementCounter.new “inc_counter”; (*INSTANTIATE OBJECT*) Class_DecrementCounter.new “database”; (*ADD LINK *) RuntimeLib.addLink (“inc_counter”, “database”); 実行系列のソースコードの生成 テスト用スクリプトを作成して、 プロトタイプ実行環境でテスト 平成13年3月7日

検証支援環境 F-Verifier 1.構築した分析モデルから公理系を自動生成 2. HOLのデータ型オブジェクトの属性やメソッドを容易に表現 3. Model Builderと連携して、検証に必要な表明群の導入 4. HOLによるインタラクティブプルーフ HOLによる表現を割り当てる 公理系自動生成器＆ HOLインタプリタ -対話的な証明を行う。 検証に必要な表明群を導入する 平成13年3月7日

リアクティブシステムモデルObTSと実行環境 リアクティブシステムモデルObTS、言語ObCL、実行システムObML ObTS ：Statechartモデルのオブジェクト指向化 統合モデル＋同期型通信モデル ObML ： ML環境上での実行系 ML環境でのリアクティブシステムの設計とテスト 設計・テストスクリプトのMLでの記述 MLの豊富なデータ構造、高階関数を利用した設計・テストスクリプトの構成と再利用 他のML-based　ツールとの結合：　HOL，Design CPN 実用規模問題の記述 ＩｒＬＡＰ、TCPIP 北陸先端大「ソフトウェア設計論」で200名の学生が利用 平成13年3月7日

リアクティブシステム 記述対象システムの世界 ObTS(ツール)の世界 外部環境 スクリプト化 モデル化 平成13年3月7日 ランダムイベント列生成 網羅的イベント列生成 リアクティブシステム （例：エレベータシステム） 記述対象システムの世界 ObTS(ツール)の世界 オブジェクト(状態遷移図)と オブジェクト間通信 外部環境 （例：エレベータの利用者） 刺激（ボタン押下） 応答（エレベータの移動） 動作解析器 スクリプト化 モデル化 動作スクリプト ObMLコード シミュレータエンジン Standard ML 動作解析器 イベント列 生成器 動作 結果 ObCL コンバータ 記述 解析 フィードバック 平成13年3月7日