タグ: 形式仕様記述

MTSAチュートリアル： 人工知能技術を応用したソフトウェア仕様自動生成ツール(1/24)

投稿日時: 投稿者: topse-center

セミナー概要

タイトル：
MTSAチュートリアル： 人工知能技術を応用したソフトウェア仕様自動生成ツール
日時：
2017年1月24日(火)
13:30-17:00（受付開始: 13:00）
会場：
国立情報学研究所 20階 ミーティングルーム(2009/2010)
概要：
MTSA(The Modal Transition System Analyzer)はインペリアル・カレッジ・ロンドンとブエノスアイレス大学で共同開発された，ソフトウェア仕様の自動生成ツールです．形式的に記述された環境モデルと要求モデルを入力とし，正しさが保証された仕様モデルをゲーム理論に基づいて自動生成します．本セミナーではMTSAの開発者であり，ソフトウェア工学分野の若手トップクラスの研究者であるブエノスアイレス大学のNicolas D’Ippolito助教によるMTSAチュートリアルを行います．

1. Introduction to behaviour models
2. Modelling concurrency.
3. Brief intro to linear temporal logics
4. Controller synthesis in MTSA
5. Enactment of controllers

MTSA: http://mtsa.dc.uba.ar
本講義は英語にて行われます．

講師
　Nicolas D’Ippolito助教, ブエノスアイレス大学
　http://lafhis.dc.uba.ar/en/~dippolito

定員：
30名(先着順)
※定員に達し次第，申し込みを締め切らせていただきます。
参加費：
無料
参加申込方法：
参加申込みサイトより必要事項を入力の上、お申込みください。※こちらでPCを準備できますのでご希望の場合は申請時に選択してください。
http://ws.formzu.net/fgen/S53074529/
主催：
NPO法人 トップエスイー教育センター
協力：
国立情報学研究所 GRACEセンター
お問合せ窓口：
セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry_[at]_topse.or.jp ※_[at]_部分を@に変えてください

CafeOBJで学ぶ形式仕様記述とその証明(9/16,23)

投稿日時: 投稿者: topse-center

セミナー概要

タイトル：
CafeOBJで学ぶ形式仕様記述とその証明
日時：
2016年9月16日(金)、23日(金)
13:30-17:00（受付開始: 13:00）
会場：
国立情報学研究所 20階 ミーティングルーム(2009/2010)
概要：

CafeOBJは、代数的にシステムの仕様を記述し、その上の性質を証明することができる先端的な形式仕様言語の一つです。本講義では、CafeOBJを使った代数仕様言語の記述方法とシステムの性質を対話的に証明する方法を実際に支援ツールを使いながら学ぶことができます。

講義は2日間にわたって行われ、自然数やリストを使ったCafeOBJによる代数仕様記述の記述方法から、具体的な相互排他プロトコルを使った対話的な証明まで、ツールを通して体験していただけます。CafeOBJの開発者の一人である二木特任教授から直接学ぶことができるまたとない機会となっております。

当日会場に用意されたシンクライアントにて演習を行うことができます。ご自身のPCで動かしてみたいという方は、以下のページからCafeOBJ 1.5.5をインストールしてご持参ください。

http://cafeobj.org/download/

※本講義は、2015年10月23日に行われた内容に「仕様計算(Specification Calculus)による場合分けの自動化」の解説と演習が追加されています。

講師：北陸先端科学技術大学院大学 ソフトウェア検証研究センター 特任教授 二木厚吉

参考資料：

以下のページから最新の講義資料をダウンロードできます。http://www.jaist.ac.jp/~kokichi/lecture/1609NII/

※講義資料は英語が中心となりますが、講義は日本語で行います。

「CafeOBJ入門」
(1) 形式手法とCafeOBJ: http://ci.nii.ac.jp/naid/110006664762
(2) 構文と意味: http://ci.nii.ac.jp/naid/110006664763
(3) 等式推論と項書換システム: http://ci.nii.ac.jp/naid/110006840405
(4) 証明譜による検証法: http://ci.nii.ac.jp/naid/110006990888
(5) 認証プロトコルの検証: http://ci.nii.ac.jp/naid/130004549136
(6) 通信プロトコルの検証: http://ci.nii.ac.jp/naid/10025982447

スケジュール：
9月16日(金)
13:30 – 15:00 講義1: CafeOBJの概要と基礎, 自然数の表現
15:15 – 16:45 講義2: リスト・シーケンス・集合と仕様計算(Specification Calculus)
16:45 – 17:00 質疑応答
9月23日(金)
13:30 – 15:00 講義3: CafeOBJによるモデリングと記述の実際
15:15 – 16:45 講義4: CafeOBJによる証明の記述と証明の実際
16:45 – 17:00 質疑応答
定員：
16名(先着順)
※定員に達し次第，申し込みを締め切らせていただきます。
参加費：
会員 無料／一般 16,000円／学生 3,000円
※NPO法人 トップエスイー教育センター会員および日本ソフトウェア科学会会員の方は、会員価格で参加いただけます。
参加申込方法：
参加申込みサイトより必要事項を入力の上、お申込みください。※こちらでPCを準備できますのでご希望の場合は申請時に選択してください。
https://ws.formzu.net/fgen/S29943907/
主催：
NPO法人 トップエスイー教育センター
協力：
国立情報学研究所 GRACEセンター
協賛：
日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ窓口：
セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry_[at]_topse.or.jp ※_[at]_部分を@に変えてください

JSTMセミナー：仕様とテストを行き来してアジャイル・形式手法・テスト自動生成を考える(12/5,7)

投稿日時: 投稿者: topse-center

セミナー概要

日時：
2014年12月5日(金)，7日(日)
ともに9:30-17:30（受付開始: 9:00）
※5日と7日の内容は同一です。
会場：
国立情報学研究所 国立情報学研究所 20階 ミーティングルーム(2009/2010)
概要：
ますます困難となるソフトウェア開発の課題に対し，以下のように様々な立場・視点からの取り組みがなされています．
・ アジャイル開発のための，テスト（動作例）を軸としたテスト駆動開発やその発展手法
・ 厳密な言語による記述に基づく仕様の厳密化やツールによる検証（形式手法）
・ 様々な技法を用い系統的に行う品質保証テストやその自動生成ツール
これらの分野は互いに関係ない，時には相反するものだと見なされているかもしれません．しかし，これらの分野はすべて，

「ソフトウェアが実現すべき機能」を定義する，そしてその定義を用いて確かに実現がされていることを検証・確認する

という共通の課題に向き合っているものです．このため，これらの分野それぞれで積み上げられた技術や考え方は，元となる思想が異なるからこそ，互いの課題を解決する可能性があります．

本セミナーでは，ソルバー（モデル発見）ツールを用いて，「仕様を基にテストケース（動作例）を生成や確認する」，あるいは「テストケース（動作例）を基に仕様を確認する」演習を行います．この演習は上記の3つの分野にまたがって行うもので，それぞれの分野での上記課題に対する考え方への入門となるとともに，それら分野の相互関係・相互補完について広い視点から学び，議論する内容となります．

本セミナーで用いるツールは，情報処理推進機構（IPA）のソフトウェア工学分野の先導的研究支援事業（RISE)の委託研究により試作したものです．Java言語で書いたデータ構造やインターフェースの記述に対し，仕様や場合分けのヒント，動作例などを付加することで，手軽にソルバー（モデル発見）の技術を，インクリメンタルに，インタラクティブに活用できるようになっています．

【注意事項】
・ ツールをインストールしたWindows PCを用意する予定です．
・ テスト駆動開発（TDD）やその発展（受け入れテスト駆動開発ATDDなど），VDMやAlloyなどの形式仕様記述手法，PICTなどのテスト自動生成ツールなどの知識・経験があれば，より理解が深まりますが，必須ではありません（これらの分野への導入をしつつ，相互の関係について考える内容となっています）．

講師：
・石川 冬樹 准教授（国立情報学研究所）
定員：
35名(先着順)
※定員に達し次第，申し込みを締め切らせていただきます。
参加費：
無料
※NPO法人 トップエスイー教育センター会員の方は、優先的に受講いただけます。
参加申込方法：
参加申込みサイトより必要事項を入力の上、お申込みください。
http://ws.formzu.net/fgen/S57176756/
主催：
NPO法人 トップエスイー教育センター
協力：
国立情報学研究所 GRACEセンター
お問合せ窓口：
セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry@topse.or.jp

Event-B/RODIN集中セミナー（11/15-16）[終了]

投稿日時: 投稿者: topse-center

セミナー概要

日時：
(1)2013年11月15日(金) 10：00-12:00
産業界での経験に関する講演
(2)2013年11月15日(金) 13：00-17:00
Event-B/RODINセミナー（基礎編）
(3)2013年11月16日(土) 13：00-17:00
Event-B/RODINセミナー（発展編）
(それぞれ開始30分前より受付開始)
※ 部分的にご参加いただくこともできます。詳細はプログラムをご参照下さい。
※ セミナー(2)/(3)についてはPCをご持参下さい．
会場：
国立情報学研究所 12階 会議室(1208/1210)
概要：
ソフトウェアの信頼性を効率よく高めるためには，上流工程の時点における取り組みが重要とされます．実装やテストに至る前に，不具合の元となる曖昧さや不整合を，仕様など上流工程の成果物の時点で排除するという考え方です．これに対して日本国内では近年，厳密な言語を用いたモデル記述と検証を行う形式手法が注目されています．フェリカネットワークでのVDM手法の適用事例がよく知られています．
一方欧州を中心に，ソフトウェア外の環境も含めたシステム全体の記述，仕様の複雑さの分解といった特徴を持つEvent-B手法が盛んに取り組まれています．DSFにおけるガイダンス，IPAによる実証実験などEvent-Bは用いられています（下記リンク参照）．
本セミナーは，Event-B活用の支援ツールRODINの研究開発におけるコーディネーターを務めたA. Romanovsky教授をはじめとし，欧州から4人の専門家を招いてEvent-Bに関する講演，セミナーの場を設けます．産業界での経験に関する講演をはじめ，実際にツールを利用したEvent-B/RODINセミナーを基礎編，発展編と開催いたします．

一部のみの参加も可能となっていますので，ぜひふるってご参加下さい．

※ 講演，セミナーは英語にて行われますが，日本人のアシスタントが必要に応じお手伝いをします．

参考リンク
http://www.event-b.org/
http://www.nttdata.com/jp/ja/dsf/
http://www.ipa.go.jp/sec/softwareengineering/reports/20120420.html

講師：
Alexander Romanovsky 教授（ニューカッスル大学・イギリス）
Alexei Iliasov 博士（ニューカッスル大学・イギリス）
Elena Troubitsyna 准教授 （オーボ・アカデミー大学・フィンランド）
Linas Laibinis 講師 （オーボ・アカデミー大学・フィンランド）
石川 冬樹 准教授（国立情報学研究所）
プログラム：
(予定）
（１） 産業界での経験に関する講演
11/15 （金）10:00-12:00

この講演では，欧州でのEvent-B手法に関する産業界での経験について報告をします．実際のプロジェクト，パイロットプロジェクトに関し，異なる抽象度でのどのような側面をモデル化・リファインメントしたのか，どのような性質を検証したのか，どう効率的な活用を目指したのかなどについて議論します．

対象：形式手法に関し，技術詳細ではなく応用アプローチに興味がある方々
VDMによる仕様記述やフェリカネットワークの事例など，形式手法やその応用に関する知識や技術的な経験があれば理解が深まると考えられますが，必須ではありません．

（２）Event-B/RODINセミナー（基礎編）
11/15 （金） 13:00-17:00

このセミナーでは，Event-B手法とその活用を支援するツールRODINに関する入門を行います．Event-Bは，複雑な構造と振る舞いを徐々に導入し（段階的詳細化），厳密な仕様を構築するための手法です．最終的に得られる全体的な仕様が正しくなるように，各段階でのモデルに対して検証を行っていきます（Correctness by Construction）．

対象： Event-BとRODINツールについて学習，利用をしてみたい技術者の方々．VDMなど他の形式手法や，厳密な仕様記述に関する基礎知識（命題論理，一階述語論理など）に関する事前の経験があれば理解が深まると考えられますが，必須ではありません．

（３）Event-B/RODINセミナー（発展編）
11/16 （土） 13:00-17:00

このセミナーでは，Event-B手法とRODINツールを用いた検証について，発展的な議論と体験を行います．特に，安全性分析や耐故障性のモデル化など，システムディペンダビリティのためのモデル化と検証について，詳細な検討を行います．

対象： Event-Bを用いた検証についてより深い理解を得たい技術者の方々
前日の基礎編セミナーに参加できない場合でも，前日の資料を自習用に送付するなど，可能な限り補足を行うようにします．その場合，自習を行うために，他の形式手法や，厳密な仕様記述に関する基礎知識（命題論理，一階述語論理など）に関する事前の経験があることが望ましいです.

定員：
60名
※原則先着順としますが，ＮＰＯ法人トップエスイー教育センター、日本ソフトウェア科学会の会員の方は優先的に受講いただけます。定員に達し次第，申し込みを締め切らせていただきます。
参加費：
無料
参加申込方法：
下記サイトよりお申込みください。
http://form1.fc2.com/form/?id=631867
主催：
NPO法人 トップエスイー教育センター
協力：
国立情報学研究所 GRACEセンター
協賛：
日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ窓口：
inquiry@topse.or.jp

Alloy Analyzerによるモデリング入門(1/18開催)(終了)

投稿日時: 投稿者: topse-center

セミナー概要

定員になりましたので、募集を締め切らせて頂きます。お申込み頂き、有難うございました。

日時：
2013年1月18日(金) 13:00-17:00(受付開始: 12:30)
会場：
国立情報学研究所 20階 ミーティングルーム1・2(2009,2010)
概要：
　本セミナーでは、高度な数学的知識を駆使せずに、形式手法ツールを有効に利用してモデリングする方法を考えていきます。形式手法の最大のメリットは、数学的厳密さを利用した、間違いの少ない開発を行えることにあります。一方で、メリットを生かすには、利用者側の知識、および技法やツールに対するスキルが重要になってきます。本セミナーでは、形式手法ツールの一つであるAlloy Analyzer (http://alloy.mit.edu/alloy/)を用いて、そのスキルを学びます。
　Alloy Analyzerは、数ある形式手法ツールの中でも、シンプルで扱いやすいツールの一つです。Alloy Analyzer は必要とする前提知識が少なく、また試行錯誤のしやすい仕組みになっており、初心者でも扱いやすい形式手法ツールと言えます。
　本セミナーでは、前半にてAlloy Analyzerを使う上での簡単なコツを学びます。後半では、演習を通して、形式手法のメリットを体験していただけます。
【スケジュール】(詳細項目は変更される可能性があります)
1. Alloy Analyzer概論
　- Alloy Analyzerの特徴
　- Alloy Analyzer文法速習
　- Alloy Analyzerモデル実例紹介
2. Alloy Analyzerモデリング演習
　- 簡単なWebアプリケーションの開発例を用いて、Alloy Analyzerによるモ
　デリングを体験します。
【参考書】(お持ちいただく必要はありませんが、あれば理解が深まります)
　1. 抽象によるソフトウェア設計 Alloyではじめる形式手法, オーム社, 2011
【演習環境】
　当日、既にAlloy Analyzerがインストールされたシンクライアントにより演習をして頂けます。ご自身のPCを持ち込んでの演習をご希望の方は、下記のページに従い、Alloy AnalyzerおよびJava実行環境をあらかじめインストールして参加ください。
– Alloy Analyzer(http://alloy.mit.edu/alloy/download.html)
– Java SE(http://www.oracle.com/technetwork/jp/java/javase/overview/index.html)
講師：
・小林健一(株式会社豆蔵)
定員：
25名(先着順)
※定員になりましたので、募集を締め切らせて頂きます。お申込み頂き、有難うございました。
参加費：
無料
参加申込方法：
参加申込みサイトより必要事項を入力の上、お申込みください。
※定員になりましたので、募集を締め切らせて頂きます。お申込み頂き、有難うございました。
http://form1.fc2.com/form/?id=631867
主催：
NPO法人 トップエスイー教育センター
協力：
国立情報学研究所 GRACEセンター
お問合せ窓口：
セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry@topse.or.jp
 
 
 

【TopSE特別講義】「定理証明と検証」(3/22開催)[終了]

投稿日時: 投稿者: topse-center
■日　程：2012年3月22日(木) 10:30-18:00
　　　　　　　　3月23日(金) 10:30-16:15（2日間）
■会　場：国立情報学研究所 20階　ミーティングルーム1・2（2009・2010）
※定員に達したためお申込を締め切りました。

セミナー概要
日　時 2012年3月22日(木) 10:30-18:00、
3月23日(金) 10:30-16:15（2日間）
会　場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
〒101-8430 東京都千代田区一ツ橋2-1-2
概　要 ソフトウェアの不具合を防ぐ技術として，定理証明器を使った検証技術が注目されています．この技術は形式手法の一種であり，実際に動作するプログラ ムのふるまいが正しいことをを保証することができます．同じく形式手法に分類されるモデル検査技術と比較して，潜在的な適用範囲ははるかに広く強力な手法 ですが，その分使いこなすには熟練が必要であると言われています．本講義では，定理証明器の一つであるCoqをとりあげます．Coqは，強力な仕様記述能力を持ち，また証明を支援する機構を備えています．講義は検 証技術の基本から始め，Coq を使った関数型プログラミングの手法やタクティックを使った証明の技法を学んでいきます．さらに，企業での取り組みや例題を交えながら実際のプロジェクト に適用する際の問題点や注意点についても紹介します．その際，講師自身が開発した，Java や Scala と連携するためのcoq2scala 機能を使用して，証明されたプログラムを既存のプロジェクトに導入する方法についても説明します．

【前提知識】
とくに必須となる前提知識はありませんが，MLやHaskellなどの関数型言語の知識があれば理解の助けになるでしょう.

【講義スケジュール】
2012年3月22日(木) 10:30-18:00 (4コマ)
2012年3月23日(金) 10:30-16:15 (3コマ)

【講　師】
今井 宜洋 氏 (有限会社ITプランニング)

※フィードバックをいただく目的で，参加費を無料に設定させていただいております．講義終了後のアンケートにご協力ください．
※本講義は、トップエスイーの講義です。今回特別にNPO会員の皆様にも聴講していただけます。
なお，1日目(3/22)の講義終了後に講義室にて簡単な懇親会を行います (千円程度の参加費を頂戴いたします) ので，お時間のある方は是非ご参加ください．
内容のレベル 入門
参加費 無料
※NPO法人 トップエスイー教育センター会員は優先的にご参加いただけます。
定　員 30名(先着順)
※定員に達し次第，申し込みを締め切らせていただきます。
申込方法 参加申込みサイトより必要事項を入力の上、お申込みください。
※定員に達したためお申込みを締め切らせていただきました。
主　催 国立情報学研究所 GRACEセンター, NPO法人 トップエスイー教育センター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry@topse.or.jp

VDM、SPINから始める形式手法入門(8/8-12開催)[終了]

投稿日時: 投稿者: topse-center

■日　程：2011年8月8日(月)-12日(金) 各日とも17:30-19:30(17:00受付開始)
※初日のみ参加も可能です。
■会　場：国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講　師：国立情報学研究所　石川　冬樹，田辺　良則
■参加費：一般会員 無料、一般非会員 18,000円（税込み）
学生会員 無料、学生非会員 10,000円（税込み）
※初日のみ参加の場合、参加費は無料です。
※一般・学生非会員の参加費の記載が誤っておりました。お詫びいたします。(8月2日訂正)

セミナー概要
日　時 2011年8月8日(月)-12日(金) 各回　17:30-19:30(17:00受付開始)
会　場 国立情報学研究所 20階 ミーティングルーム１・２(2009, 2010)
概　要 近年，ソフトウェア開発における効率的な信頼性向上のためのアプローチとして，形式手法が注目され話題になっています．一方で，言葉は聞いたことがあってもなかなか実際に自身で触れる機会がなく，ニーズに合うものなのかよくわからないという方も多いのではないかと思います．また「形式手法」とはあくまでアプローチの総称であり，実際の活用においては多様な手法・ツールから問題に適したものを選んだり，その活用方針を議論し定めていったりする必要があります．本セミナーでは，まず形式手法の考え方を知るため，また実感するため，代表的な手法・ツールとしてVDM，SPINの概要を紹介するとともに，それらを使った簡単な演習を行います．加えて，それらとの比較を通して他の手法・ツールの概要についても紹介するとともに，近年盛んに公開されている応用事例の調査報告や適用ガイダンス等についても紹介します．各回の構成は下記の通りです．

8/8（月）1日目：形式手法概論
・ 形式手法の位置づけ・基本的な考え方
・ VDM，SPINの位置づけ・基本的な考え方

8/9（火） 2日目：VDM++入門
・ VDM++言語，Overture IDE/VDMToolsを用いた形式仕様記述入門，演習

8/10（水）3日目：SPIN入門
・ SPINを用いたモデル検査入門，演習

8/11（木） 4日目：形式手法ツール概論
・ VDM，SPINと対比しての様々な手法・ツールの紹介

8/12（金） 5日目：応用事例紹介
・ 応用事例の調査報告や適用ガイダンス等の紹介

内容のレベル 入門
講　師 石川　冬樹，田辺　良則
対　象 一般　※　定員 36 名（先着順）
参加費 一般会員 無料、一般非会員 18,000円（税込み）
学生会員 無料、学生非会員 10,000円（税込み）
※初日のみ参加の場合、会員種別に関わらず参加費は無料です。
※NPO法人 トップエスイー教育センター会員は会員としてお申込ください。
※参加費の一部（10%）を、東日本大震災の義援金として寄付いたします。
※「会員」：NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会に所属されている方は会員割引の対象となります。
主　催 NPO法人 トップエスイー教育センター
協　力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

Coqで学ぶ定理証明入門(7/12開催)[終了]

投稿日時: 投稿者: topse-center

■日　程：2011年7月12日（火）
■会　場：国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講　師：(有)ITプランニング 今井宜洋

セミナー概要
日　時 2011年7月12日（火） 10:00-17:00(9:30受付開始)
会　場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概　要 ソフトウェアの不具合を防ぐ技術として定理証明器を使った検証技術が着目されています。定理証明器は実際に動作するプログラムのふるまいを保証できる形式手法です。特にその一つであるCoqは強力な仕様記述能力を持ちながら、証明を支援する機構を備えています。本セミナーでは、検証技術の基本からCoqを使った関数型プログラミングのテクニックと、タクティックを使った証明の技法までを学びます。さらに、企業での取り組みや例題を交えながら既存のプロジェクトで運用するときの問題や注意点について考えていきます。

なお、本セミナーでは、会場に設置されたシンクライアントを使いCoqの演習を行います。もし、ご自身のPCで演習されたい場合は、下記を参考にCoqの環境をインストールし、ご持参ください。
http://www39.atwiki.jp/fm-forum/pages/16.html

内容のレベル 入門、形式仕様記述
講　師 (有)ITプランニング 今井宜洋
対　象 一般　※　定員 36 名（先着順）
参加費 一般会員 無料、一般非会員 16,000円（税込み）
学生会員 無料、学生非会員 8,000円（税込み）
※会費の一割は、東日本大震災の義援金に寄付いたします。
※NPO法人 トップエスイー教育センター、日本ソフトウェア科学会の会員の方は割引の対象となります。
受講料は当日受付にて現金でお支払いください．その他の支払い方法をご希望の方は，事前にメールで inquiry@topse.or.jp までお知らせください．
主　催 NPO法人 トップエスイー教育センター
協　力 国立情報学研究所 GRACEセンター
協　賛 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ先 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

【TopSEチュートリアル】VDM++による形式仕様記述(1/25開催)[終了]

投稿日時: 投稿者: topse-center

■日　程：2011年1月25日(火)
■会　場：国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講　師：石川　冬樹 (国立情報学研究所)

セミナー概要
日　時 2011年1月25日(火) 10:00-17:00 （受付開始：9:30）
会　場 国立情報学研究所 20階 ミーティングルーム1・2（2009・2010）
概　要 本チュートリアルでは，形式手法VDM++によるソフトウェアの仕様記述と検証・分析について，ツールを使った実習を交えて解説します。
ソフトウェア開発では，開発の早い段階での誤りが後の工程へと引き継がれることに起因する，システムの信頼性低下や手戻りによるコスト増大が大きな問題となっています．このため，開発の初期段階の仕様書や設計書等の中間成果物に対して，科学的・系統的に分析・検証を行い誤りを除いておくことが重要であると考えられます．そのためのアプローチとして，数理的な基礎のもとにモデル化と検証・分析を行う，形式手法が最近注目されています．しかし，これまで開発者 が身につけてきたものとは異なる知識・スキルが求められるので，敷居が高いという側面があるのも事実です．
本チュートリアルでは，ライトウェイトな形式手法であるVDMをとり上げます．VDMでは，システムの状態を表す変数やそれに対する操作を抽象的にモデル化し，インタプリタ実行によるテストを中心とした方法で検証・分析を行います．このため，一般の開発者にとって身近な方法により，実装詳細を捨象した形での仕様の厳密化・明確化，および実行を通した検証・分析を行うことができます．
また，形式手法としてのVDMの考え方・アプローチと，オブジェクト指向に基づいたVDM++言語を使った仕様記述について，解説します．さらに，ツールを用いた仕様の実行と検証・分析方法についても，具体例に基づく実習と実演を交えて，説明します．
内容のレベル 初級
講　師 石川冬樹 (国立情報学研究所)
対　象 一般※　定員 32 名（先着順）
参加費(税込) 一般会員 10,000円、一般非会員 15,000円
学生会員 3,000円、学生非会員 6,000円
※NPO法人 トップエスイー教育センター、日本ソフトウェア科学会の会員の方は割引の対象となります。
※GRACEセンター協賛企業の方は別途お問い合わせ下さい。
NPO法人 トップエスイー教育センターへ入会を希望される方は、備考欄に「NPO法人入会希望」とご記入ください。会員価格にてご参加いただけます。なお、会費（年会費12,000円）は会場受付にてお支払ください。
主　催 日本ソフトウェア科学会
協　力 NPO法人 トップエスイー教育センター
国立情報学研究所 GRACEセンター
株式会社　CSK
お問合せ先 本セミナーに関するご質問などは、下記アドレスにて承ります。
vdm-tutorial@topse.jp

【TopSEナイトセミナー】 ソフトウェア工学入門－４日で学ぶソフトウェア工学(2/18, 26, 3/4, 11開催)[終了]

投稿日時: 投稿者: topse-center

■日　程：
第１夜　2010年 2月18日(木) 17:30-20:40
第２夜　2010年 2月26日(金) 17:30-20:40
第３夜　2010年 3月 4日(木) 17:30-20:40
第４夜　2010年 3月11日(木) 17:30-20:40
■会　場：国立情報学研究所 20階

セミナー概要
日　時 第１夜　2010年 2月18日(木) 17:30-20:40
第２夜　2010年 2月26日(金) 17:30-20:40
第３夜　2010年 3月 4日(木) 17:30-20:40
第４夜　2010年 3月11日(木) 17:30-20:40
会　場 国立情報学研究所 20階
概　要 ソフトウェア工学に関する連続セミナー(４回）を開催します。本セミナーでは、ソフトウェア工学の基本的なトピック（要求分析、設計、プロジェクトマネージメント、形式手法）ごとに専門講師陣が分かりやすく解説します。ソフトウェアにおける要求とは何か？設計をうまく行うにはどうすれば良いか？プロジェクトを円滑に進めるポイントは？フォーマルメソッドとは？など、基礎的な知識を押さえておきたいという方は是非参加ください。完全オムニバス形式ですので、お好きなトピックだけ参加することも可能です。

  • 第１夜 2月18日(木) 17:30-20:40
    • ソフトウェア工学概論 (吉岡 講師, 国立情報学研究所)
    • 要求工学入門 (白銀 講師, 東京女子大)
  • 第２夜 2月26日(金) 17:30-20:40
    • UML入門、アーキテクチャパターンとデザインパターン (鄭 講師, 早稲田大学)
    • 再利用の有用性とプロダクトライン型開発概論 (位野木 講師, 東芝ソリューション)
  • 第３夜 3月 4日(木) 17:30-20:40
    • プロジェクトマネージメント概論 (白川 講師, NTTデータ先端技術)
  • 第４夜 3月11日(木) 17:30-20:40
    • フォーマルメソッド概論（石川講師, 国立情報学研究所）

※本セミナーはトップエスイーの講義ではありませんので、単位は取得できません。
定　員 35名(先着順)
受講料金 一般会員　 10,000円
一般非会員 15,000円
学生会員　 5,000円
学生非会員 7,000円

※当日会場にて現金でお支払い下さい。領収書を発行します。
※NPO法人 トップエスイー教育センター会員および協力団体の方は「会員」価格となります。
※受講料には教科書代金を含みます。
※国立情報学研究所が主催するトップエスイーに入学予定の受講生の方は無料です。申し込み時にお知らせください。
主　催 NPO法人 トップエスイー教育センター
協　力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp