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

Slides:



Advertisements
Similar presentations
Division of Process Control & Process Systems Engineering Department of Chemical Engineering, Kyoto University
Advertisements

ソフトウェア工学 知能情報学部 新田直也. オブジェクト指向パラダイムと は  オブジェクト指向言語の発展に伴って形成され てきたソフトウェア開発上の概念.オブジェク ト指向分析,オブジェクト指向設計など,プロ グラミング以外の工程でも用いられる.  ソフトウェアを処理や関数ではなくオブジェク.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
メタモデル記述を用いた成果物間の依存関係追跡手法
システム開発におけるユーザ要求の 明示的表現に関する一検討
モデル検査の応用 徳田研究室 西村太一.
シーケンス図の生成のための実行履歴圧縮手法
東京工科大学 コンピュータサイエンス 亀田弘之
Riding the Design Wave II
表計算ソフトで動作するNEMUROの開発
リアルタイムシステムに 上流設計ツールは有効か?
プログラミングパラダイム さまざまな計算のモデルにもとづく、 プログラミングの方法論 手続き型 関数型 オブジェクト指向 代数 幾何.
LMNtalからC言語への変換の設計と実装
肥後 芳樹, ○石尾 隆, 渡邊 結, 出張 純也, 畑 秀明, 三宅 達也, 水野 修, 丸山 勝久
確率モデルによる 画像処理技術入門 --- ベイズ統計と確率的画像処理 ---

UMLの概要と オブジェクト指向の 基本概念
ソフトウェア設計における意思決定ガイドラインとしてのデザインパターンのモデル
SS2009 形式手法の適用ワーキング グループの報告
CSP記述によるモデル設計と ツールによる検証
リファクタリングのための 変更波及解析を利用した テスト支援ツールの提案
高山建志 五十嵐健夫 テクスチャ合成の新たな応用と展開 k 情報処理 vol.53 No.6 June 2012 pp
UML入門 UML PRESS vol.1 より 時松誠治 2003年5月19日.
UMLとは           032234 田邊祐司.
チーム FSEL 立命館大学情報理工学部 ソフトウェア基礎技術研究室
オブジェクト指向プログラムのための 動的結合メトリクスの評価
UMLメタモデルの変更に対応した ダイアグラム間整合性検証環境の 自動生成手法
組込みシステムの外部環境分析のためのUMLプロファイル
朝日大学大学院 経営学研究科 奥山 徹 データベース論 朝日大学大学院 経営学研究科 奥山 徹 2006/05/22 データベース論(6回目)
ソフトウェアを取り巻く環境の変化がメトリクスに及ぼす影響について
只見町 インターネット・エコミュージアムの「キーワード」検索の改善
アスペクト指向に基づく 拡張可能な MDAモデルコンパイラ
社会シミュレーションのための モデル作成環境
コードクローン検出ツールを用いた ソースコード分析システムの試作と プログラミング演習への適用
プログラム動作理解支援を目的とした オブジェクトの振舞いの同値分割手法
ソフトウェア設計検証 研究室の紹介 知能情報学部 准教授 新田直也.
オープンソース開発支援のための ソースコード及びメールの履歴対応表示システム
UMLモデルを対象とした リファクタリング候補検出の試み
コードクローン検出に基づくデザイン パターン適用支援手法の提案と実現
知能情報システム特論 Introduction
片方向通信路を含む ネットワークアーキテクチャに於ける 動的な仮想リンク制御機構の設計と実装
背景 課題 目的 手法 作業 期待 成果 有限体積法による汎用CFDにおける 流体構造連成解析ソルバーの計算効率の検証
ソフトウェア開発における形式化技術と環境
Java における 先進的リフレクション技術
コードクローン分類の詳細化に基づく 集約パターンの提案と評価
UMLの概要とオブジェクト指向の基本概念
モデル検査(5) CTLモデル検査アルゴリズム
JAVAバイトコードにおける データ依存解析手法の提案と実装
環境モデリングによるモデル検査スクリプトの自動生成
並列処理プロセッサTPCOREの 組み込みシステムへの応用 理工学研究科数理情報科学専攻 福永 力,岩波智史,情報システム研究室.
INTRODUCTION TO SOFTWARE ENGINEERING
オブジェクトの協調動作を用いた オブジェクト指向プログラム実行履歴分割手法
ソフトウェア工学 知能情報学部 新田直也.
All Rights Reserved, Copyright © 2004, Kobayashi
メソッドの同時更新履歴を用いたクラスの機能別分類法
開発作業の形式化に基づく プロセス評価 松下誠 大阪大学.
ソフトウェア工学 知能情報学部 新田直也.
ソフトウェア工学 理工学部 情報システム工学科 新田直也.
蓄積されたオブジェクトの動作履歴を用いた 実行履歴削減手法の提案
データ中心システム設計方法論“DATARUN” 
UMLモデルを対象とした リファクタリング候補検出手法の提案と実現
ソフトウェア工学 知能情報学部 新田直也.
エイリアス関係を考慮した Javaプログラム用静的スライシングツール
複雑度メトリクスを用いた JAVAプログラム品質特性の実験的評価
ソフトウェア工学 知能情報学部 新田直也.
コードクローン解析に基づく デザインパターン適用候補の検出手法
知識ベースの試作計画 ●●●研究所 ●●●技術部 稲本□□ 1997年1月.
オブジェクト指向言語における セキュリティ解析アルゴリズムの提案と実現
オブジェクト指向メトリクスを用いた 開発支援に関する研究 --- VC++とMFCを用いた開発を対象として ---
1.2 言語処理の諸観点 (1)言語処理の利用分野
Presentation transcript:

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

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

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

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

北陸先端科学技術大学院大学 要求分析、ソフトウェア発展 問題 P 実世界 W 東京大学 仕様書 モーバイル言語、 安全性 東京工業大学 形式的オブジェクト指向方法論 ソフトウェア発展方式、メカニズム 実世界 W 東京大学 仕様書 モーバイル言語、 安全性 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件 新聞報道 査読つき論文総数 178 招待講演、論文   21件 特許   (二村グループ) ランダムデータジェネレータ生成方式およぶそのプログラム 連結グラフの生成方式およびそのプログラム 出願準備中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日

形式的オブジェクト指向方法論 形式的アプローチ 仕様やモデルを数学的対象としてとらえる。 オブジェクト指向方法論への形式的アプローチ 「形式的方法論」のオブジェクト指向化 オブジェクト指向 Z、代数的アプローチ、VDM、・・・ 現実のオブジェクト指向方法論の実際とは方向性が異なる。 現実に行われているオブジェクト指向方法論の形式的アプローチが必要。 平成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:有限領域についての「軽い」整合性検証 NASA、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 実用規模問題の記述 IrLAP、TCPIP 北陸先端大「ソフトウェア設計論」で200名の学生が利用 平成13年3月7日

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