トップエスイーチャンネル(TopSE Channel)

トップエスイーチャンネル(TopSE Channel)では、次世代の中核人材となる「スーパーアーキテクト」を育成する「トップエスイー(TopSE)」プロジェクトの講義情報を紹介しています。

ここで紹介しているトップエスイーの講義は、開発深知のサイトでご覧いただけます。講義の閲覧にはユーザ登録(無料)が必要です(登録方法はこちら)。

トップエスイーでは、ソフトウェア開発方法について、理論だけでなく事例演習を交えた実践的な講義を行っています。

トップエスイーの講義は様々なコースが用意されており、ソフトウェア開発の方法について様々な角度から学習することができます。

  • 共通科目
  • プロジェクトマネジメントコース
  • 要求工学コース
  • アーキテクチャコース
  • モデル検査コース
  • 形式仕様記述コース
  • クラウドコース

トップエスイーチャンネルで公開している講義は、実際にトップエスイーで行われた講義と同じものです。また、いつくかの講義については、トップエスイーの講師によって開発深知用に作成された講義がございます。開発深知用に作成された講義については、学習の理解を深める小テストがついております。

開発深知用小テスト付講義

モデル検査事例演習
本講座は、モデル検査の実務を想定し、その開始から終了までの全プロセスを意識した演習を行います。
定理証明と検証
本講義では、強力な仕様記述能力を持ち,また証明を支援する機構を備えている定理証明器「Coq」をとりあげます。講義は検証技術の基本から始め、Coq を使った関数型プログラミングの手法やタクティックを使った証明の技法を学んでいきます。

トップエスイーの講義動画

形式仕様記述(セキュリティ編)
本講座では、定理証明、モデル検査と段階的詳細化というシステム検証における三つの主要技術に基づいた、セキュリティ・ポリシの検証問題を扱います。形式手法(Formal Methods)は、構文規則と意味規則が厳密に定められた形式仕様記述言語をデザイン記法として用いることで、曖昧性なく解釈できるモデル(形式仕様)を構築します。形式仕様言語の意味規則に照らし合わせて、モデルに不整合がないか、要求された特性を満たしているか、などを厳密に検証できることが長所です。
本講座では、最初にアクセス制御ポリシを強制するセキュリティ機構の段階的詳細化に基づく構築について、Event-Bを使って学びます。Event-BはBメソッドを基盤として開発されたシステム開発手法で、イベントの概念が導入されている点に特徴があります。ここでは、ポリシを強制するセキュリティ機構を、段階的詳細化を使って構築する過程について学びます。 そして、モデル検査ツールSPIN/Promelaを用いて、RBACに基づいたアクセス制御システムのモデリングと検証を演習形式で学びます。
性能モデル検証
本講座では、ネットワーク家電の制御ソフトウェアを題材とした産業ソフトウェアの性能モデル検証問題を扱います。近年ますます大規模化・複雑化するソフトウェアの設計において、特に性能面に関して、その動作の正しさを保証することがより困難になっていますが、設計モデルの性能面に関する動作の正しさを自動的に検証する性能モデル検査ツールUPPAALを使用し、実際のシステム開発に適用する方法を習得していきます。
本講座では、設計モデルとして、標準のモデル記述言語UML、特に性能面に関するモデル化を可能にするProfile for SPT (Schedulability, Performance, and Time)を採用して、入力モデルへの変換手法を習得します。さらに、実際に組込ボード上でのソフトウェア開発を通して、ソフトウェア設計検証の難しさを体感した上で、UPPAALツールの適用における難しさを解決するための検証プロセス、およびノウハウを習得していきます。
アスペクト指向開発
本講座では、従来のオブジェクト指向開発技術ではモジュール化/局所化が困難であった種々の関心事の分離を開発における上流工程から下流工程まで一貫して保つことで保守性の高いソフトウェアを高い生産性を伴って開発するために、対象問題のオブジェクト指向を発展させたアスペクト指向について解説します。
クラウド基盤構築演習
本講座では、Linuxとオープンソースソフトウェア(Eucalyptus)を利用して、IaaS(Infrastructure as a Service)クラウド基盤構築の実機演習を行います。
SMV入門
モデル検査ツールSMV、状態遷移図について学習する講義です。モデル検査器SMVを用いて独力でモデル検査を実行できる技術について習得することを目的としています。具体的には、専用言語であるSMV言語の文法の習得、検査式の作成方法の習得、モデル検査器SMVの操作方法の習得を目指します。講義では「SMV(Symbolic Model Verifier)とは何か?」という基本的な部分から解説し、小テストを通して理解を深めていく構成となっています。
基礎理論
形式手法を知る上で必要となる基礎知識について学んでいく講義です。形式手法入門としてもご覧いただけます。
また、検証可能なモデルの作成、離散数学の概念に基づくシステムのモデル化の基礎となる知識を学ぶことができる講義となっています。
具体的には、論理学、集合論、時相論理、システムの性質の記述、オートマトン、モデル検査アルゴリズム、モデル検査の実装方法、並行システム、抽象解釈、モデル検査ツールについて解説していきます。
ソフトウェア工学入門
本講義では、トップエスイープログラムにおける様々な講座を受講するための予備知識を補完するために、ソフトウェア工学の基礎知識について解説します。ソフトウェア開発プロセス、要求工学、要求仕様書、UML入門、アーキテクチャパターンとデザインパターン、再利用とプロダクトライン型開発、要求分析、システム分析、形式手法入門、モデル検査などについて学ぶことができます。
クラウド実践(現在のクラウド入門)
本講座では、クラウドコンピューティング環境上での分散アプリケーション開発手法を扱います。クラウドの基盤技術、OSSによるクラウド基盤、AWS(Amazon Web Services)、Eucalyptus、Webシステムの負荷、Teracotta、Hadoop、MapReduce、シリアライゼーション、クラウド上でのMPI利用例、モデル検査ツール、状態遷移図など、クラウドに関する技術や仕組みについて網羅的に解説しています。
ソフトウェア開発見積り手法
本講座では,ソフトウェア開発のプロジェクトマネジメントで最も基本的かつ重要な工数見積り手法及び規模見積り手法とその活用について解説していきます。ソフトウェア開発における見積り手法やツールの歴史、見積りミスの原因、COCOMOII、類推法、積み上げ法、パラメトリック法、CoBRA法m見積り手法比較などについて取りあげます。
形式仕様記述(基礎編)
本講座では、形式仕様言語を用いた開発対象のモデル化の問題を扱います。本講座では、多様なモデルの中で、特に静的な情報構造にまとを絞り、形式手法を用いた系統的な開発の方法を学習します。形式手法の特徴と課題、ツールの使い方、B抽象機械記法、データ構造の表現、仕様の整合性検証、段階的詳細化、VDM-SLの基本的な概念と構文などについて解説をしています。
設計モデル検証(基礎編)
本講座では,ソフトウェア開発のプロジェクトマネジメントで最も基本的かつ重要な工数見積り手法及び規模見積り手法とその活用について解説していきます。モデル検査とテストの違い、SPIN入門、SPINによるモデル検査、進行性検査とNever claim、時相論理、状態遷移図、設計・検証プロセス、フレームワーク・テンプレートの作成、検証プロセス 検証記述、並行性の導入、デバッグと検証、抽象化、ETロボコンの事例について学んでいきます。
コンポーネントベース開発
本講座では、早期の分割統治とインタフェース中心の分析/設計を系統立てて実施するためのコンポーネントベース開発手法とプロセスを習得していきます。代表的なコンポーネントベース開発方法論(Catalysis, UML Components, KobrA)が提供する分析/設計プロセスを、プロダクトライン開発の文脈上で、ネットワーク家電システムのソフトウェア開発に適用した結果について比較評価を行い、分析/設計プロセスの有用性と適用性を議論します。議論を通してコンポーネントベース開発方法論の理解を深め、分析/設計プロセスの実用的ノウハウを体得できる効果が期待できます。
OpenStackによるクラウド基盤構築
OpenStackを利用したIaaSクラウド基盤の設計・構築・運用の基礎となる技術解説を行います。OpenStackの利用方法と内部構造の解説に加えて、実機によるハンズオンを通して、OpenStackの環境構築とIaaSクラウドの利用方法を学びます。
プロジェクトマネジメントとその支援ツール
本講義では、ソフトウェア工学をプロジェクトマネジメントの視点から体系的に説明するとともにリスク識別法やその対処方法を解説し、演習によりその手法を取得する。さらに、ソフトウェアの品質や生産性を向上させるための各種の支援ツールやプロジェクトマネジメントの支援ツールを紹介するとともに,それらの支援ツールを開発する方法を解説する。
設計モデル検証(応用)
本講座では、代表的な3つのモデル検査ツールであるSPIN、SMV、およびLTSAに対し、まず標準のモデル記述言語UMLを全面的に採用し、実際に3つのツールの利用を通して、ソフトウェア設計検証の難しさを体感した上で、設計モデルの特徴に合わせたモデル検査ツールの使い分け、およびノウハウを習得していきます。
分散処理アプリ演習
本講座では、分散処理技術として広く利用されているHadoopを通して、実際の業務に役立つ事例を中心とした題材を使用し、実践的に分散処理アプリケー ションの開発を学びます。具体的には、Hadoopの構成要素であるMapReduceや、Hadoopの周辺技術でありSQLライクなインターフェイスであるHiveについて、POSデータ分析等を題材として、解説・演習を行います。
モデル駆動開発
本講義では、モデル駆動開発がなぜ必要で、どのような開発方式なのかについて解説します。またLEGO Mindstormsで制作したロボットとモデル駆動開発ツールBridgePointを使いモデル駆動開発の理解を深めていきます。
アジャイル開発
アジャイル開発を実際に小さなアプリケーション開発で経験することにより、その手法の意味を理解し、導入のためのヒントを得ることを目的とします。受講者には、実際にチーム開発を行うワークショップScrumに基づいたチーム開発と、その開発を効果的に実現するために必要となる、テスト駆動開発、ペアプログラミングといったXPのプラクティスを体験しいきます。
形式仕様記述(応用編)
本講座では、上流工程からインプリメンテーションまでをつなぐ形式手法を用いた系統的な開発の方法を学習します。Bメソッドに加えて,VDM-SLのオブジェクト指向への拡張であるVDM++を取り上げます。
実装モデル検証
ソフトウェアプログラムの検証問題を扱う。ネットワークを介したメッセー ジ通信を通して動作する分散ソフトウェアの振る舞いを網羅的に検証する技術、および計 算機上で扱える程度の規模に検証問題を変換する抽象化技術を習得する。具体的には、Java プログラムのモデル検査ツールJava PathFinderを使用し、実際のシステム開発に適用する 方法を習得する。講義を通してモデル検査技術の理解を深め、実問題への適用能力を体得 できる効果が期待できる。
並行システムの検証と実装
本講座では、信頼性の高い並行システムを構築することを目的として、CSP, FDR, JCSPを軸に、CSPによる並行システムのモデル化、FDRによる検証、JCSPによる実装方法について解説します。
CSP :並行システムを記述・解析するための理論 (プロセス代数)
FDR :CSP理論に基づく並行システム検証ツール (モデル検査器)
JCSP :CSPのプロセスモデルの実装ツール (Javaライブラリ)
クラウド実践演習
本講義は、システムの運用を行う技術者として近年求められるクラウドの技術を活用するスキルと、それに伴って変化する開発チームの在り方を学習し、演習を通じて体験していきます。具体的にはIaaS上に構築されたアプリケーションの運用方法の理解と、IaaS上に構築したアプリケーションの活用法について解説していきます。
ビジネス要求分析
本講義では、ゴール指向モデルによるビジネス戦略の立案からシナリオやドメインモデルによる将来ビジネスモデルの構築およびビジネスモデルから情報システム構築への手順について解説していきます。
ビッグデータ管理入門
ビッグデータの解析のためのデータ管理手法について解説します。取り扱うのは、NoSQL、RDB(PostgreSQL hstore)、ドキュメント指向(MongoDB)、列指向(Cassandra)です。
ソフトウェアパターン
本講義では、ソフトウェアパターンの概念から解説し、パターンの抽出/利用やパターン指向開発プロセスとその実践、デザインパターン詳説、設計原則、フレームワークとパターン、ツール活用、パターンの広がりについて紹介します。
プログラム解析
一般的なソフトウェア開発に利用できる「形式手法に基づくプログラム解析技術」としてのJML(Java Modeling Language)について学んでいきます。Design By Contract(契約に基づく設計)の手段としてJML、単体テストの手段としてのJML、プログラムの静的検証とJMLについて解説します。

トップエスイー教育センターのセミナー

ソフトウェアエンジニアのための「機械学習理論」入門
本セミナーでは、機械学習の基本的なアルゴリズムについて、その背後にある理論を解説した上で、Pythonで実装したアルゴリズムのサンプルコードを用いたハンズオンを行います。特に、ビジネス視点でのデータ活用となる「データサイエンス」を意識した解説を行い、ビジネス活用に向けた本格的な機械学習を学ぶ土台となる知識を提供します。
ソフトウェアエンジニアのための機械学習によるデータ分析実践
本セミナーでは、機械学習によるデータ分析のプロセスを実際に手を動かしながら学んでいきます(聴講だけでも問題ありません)。講義ではPythonとR、両方の例で説明しますので、どちらか好きな方(あるいは両方)で実際に分析をしていただくことができます。
Scalaで学ぶSEのための実践的関数型言語入門
本セミナーでは、最近注目されている関数型言語であるScalaを用いて、実践で役立つソフトウェアエンジニアのための関数型言語について解説します。 Scalaは、Javaとの親和性が高く、Twitter社,LinkedIn社をはじめ多くの企業(*1)で採用されている実践的な関数型言語です。セ ミナーでは、Scalaプログラミングの演習を通して、関数型言語の考え方や、関数型言語のためのコーディングスタイルを学ぶことができます。 (*1) Scala in the Enterprise,
VDM++による形式仕様記述
本講義では、形式手法とは何かについて解説し、形式手法におけるVDMの位置づけについて確認していきます。また、VDM++ Toolboxの利用法を紹介します。
SMVで学ぶモデル検査入門
本セミナーでは、モデル検査の概要に加えて、企業での取り組みやデモ、多くの例題を交えながら初心者の方にも分かりやすく説明します。また、演習問題も用意していますので、実際にモデル検査ツールSMVを操作することで、より深い理解を得ることができます。
VDM、SPINから始める形式手法入門
近年、ソフトウェア開発における効率的な信頼性向上のためのアプローチとして、形式手法が注目され話題になっています。「形式手法」とはアプローチの総称であり、実際の活用においては多様な手法・ツールから問題に適したものを選び、その活用方針を議論し定める必要があります。本講義では形式手法の概要からツールの使い方などについて解説していきます。
プロセス分析ツールPATで学ぶ並行プロセスのモデル検査
本講義では、プロセス代数(CSP)に基づくモデル検査ツールPAT (Process Analysis Toolkit)について解説します。
Coqで学ぶ定理証明入門
本セミナーでは、検証技術の基本からCoqを使った関数型プログラミングのテクニックと、タクティックを使った証明の技法までを解説していきます。さらに、企業での取り組みや例題を交えながら既存のプロジェクトで運用するときの問題や注意点について考えていきます。
MindStormで学ぶ、UPPAALによる時間制約の検証
本チュートリアルでは,特に時間制約を扱えるモデル検査ツールUPPAALを使って検証する方法について解説します。前半では、時間に関する情報をUPPAALでモデル化し、時間制約を検証する手法の概要を説明します。また、本講義はUPPAALについてある程度知識のある方が対象となります。
DESTECSCrescendoセミナー:ソフトウェアとメカトロニクスとのco-modelingco-simulation
本セミナーではDESTECSプロジェクトの中心となるFitzgerald 教授とLarsen 教授を招き、co-modeling/co-simulationの原則や産業界での応用経験についてご講演いただくとともに、Crescendoツールの体験・演習を行います.
プロセス分析ツールPATで学ぶ並行プロセスのモデル検査 | 開発深知
本セミナーでは、プロセス代数(CSP)に基づくモデル検査ツールPAT (Process Analysis Toolkit)の基本的な使い方を理解します。実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法を解説します。

トップエスイー(TopSE)の講義公開カレンダー

トップエスイー(TopSE)の公開情報

トップエスイーに関する講義の公開情報については、
トップエスイー | 開発深知ブログ
でもご確認いただけます。

参考リンク

トップエスイー | サイエンスによる知的ものづくり教育プログラム
NPO法人トップエスイー教育センター

開発深知で公開予定のトップエスイーの講義(2015年度)

4月〜5月

6月〜7月

8月〜9月

10月〜11月

12月〜1月