ネットで授業を受けられる（修了証も）MOOC－で、大学は何のために行くのか？

まえに、
ネットで授業を受けられ（＝オープンコースウェア）
さらに、修了証も受けられる（つまり、単位として認められる）
MOOCという話をした。

ここ

日本のオープンコースウェアとか、東大のMOOCsとかをまとめてみる
http://blog.goo.ne.jp/xmldtp/e/87ac7b302a46e9a531e3af1b0e619d41


で、そのMOOCの団体が、なんかできたみたい。


JMOOC　日本オープンオンライン教育推進協議会
http://www.jmooc.jp/

---

でね、e-Learning Award Forumで、セミナーをやるらしい

11月20日（水）e-Learning Award ForumにてJMOOCセミナーを開催
http://www.jmooc.jp/news/info/p1/

それによると（以下太字は上記サイトより引用）

■講演概要

急速に進展するMOOC（大規模公開オンライン講座）の展開について世界の動向を概観 した後、東京大学がCourseraに提供している２つのコースに関する状況を報告し、それをもとにMOOCの可能性と日本における展開 の意義について述 べる。また、それを具体的に実現するための組織である日本オープンオンライン教育推進協議会の概要・第１弾のプロジェクトとして来春より NTTドコモが展 開する実証実験・東京大学情報学環反転学習社会連携講座で行うMOOCと反転学習を組み合わせる研究開発について説明する。


う～ん、ほんとうは、大学って、反転学習が当然なんだよね・・・

つまり、
先生から教わって、それをやるんじゃなくって、ですね、
家で勉強してきてから、講義を受けると・・・

まあ、大学院の授業なんかだと、自分がプレゼンして、
そこから教員＆他の院生との質疑、コメントになるんで、
反転授業なんだけど、
大学は、東大でも、講義中心なんですね・・・

---

・・・あ～Moocsとか、それ以前にですね、
お勉強しましょうよ・・・大学生！

えっ就活がいそがしくて、勉強どころではない・・・
そうですよね、そうです。

大学以外でも、学校は、自分が幸せになるためにいくんですもんね。
授業と就職、どっちが自分の幸せに大事・・・

・・・わかりました。すみません・・・

P.S ・・・じゃあ、大学も、起業して、儲かる話、
ガンガンすればいいのに。。。
（と思ったこともあったが、そんな話がわかるのなら、
　大学の先生が起業してますね！すみません・・・）

UML（主にクラス図）と、要求の形式仕様言語Event-Bの対応関係について

ここに出ていた

Introduction to UML‐B,
UML‐B Class Diagrams,
UML‐B Context Diagrams
http://wiki.event-b.org/images/UMLBClassContextDiagrams.pdf


な感じ。

ってことらしい（上記PDFの中より）

ざっくりEvent B

シリーズTOPSEのEvent-B/RODIN集中セミナーに行ってきた！
前回の続き、セミナー１日目午後

Tutorial on Event-B/Rodin-Day1

の内容をメモメモ

---

■石川先生
システムモデリングする手法
並行性が書きやすい
リファインメント

■ロマノフキー先生
　自己？他者？紹介
　へじていとしないで、すぐに何でも聞いてね

■エレナ先生
　このセミナーの２つのゴール
　　　モデリング体験：基礎的な理解
　　　EventB

フォーマルVS伝統的開発

・伝統的
　RE　設計　コーディング
　　→プロセスベース

・フォーマル
　　→プロダクトベース

・フォーマル
　　抽象モデル
　　　　高いレベルのビュー
　　リファインメント
　　　　抽象モデルの詳述
　　　　要求の構造

・歴史（繰り返しなので省略）

・EventBでモデリング
　　　刺激→反応の形
　　ステートが変わる：刺激

・Where guard Then action End

・終わらないループで
　　forever do
　　　　Event1 or
　　　　Event2 or
　　　　Event3 or ...
　　end

・Model invariant 安全な許されているステート

・event-B
　マシーン
　　変数
　　変数間の関係

　コンテキスト
　　axioms,テキスト

・事例；チケットシステム
変数２つ

イベント
　　初期
　　チケットとる
　　Serve_Next：ボタン押したとき？

検証
　I (s,c,v) ∧ G(s, c, v)∧ R(s, c, v, v') →I (s, c, v')
I　不変条件
G　ガード
R　イベントアクション（反応）

---

■リーナス先生

Rodinプラットフォーム
Rodinを立ち上げ
コンポーネント
コンテキストを開く
マシーンを開く
　　モデルはいろいろ編集できる
　　　　右ボタン
　　　　エディタ内で右ボタン
　　　　もちろん、エディタで編集できる

そのほか、ツールを説明してくれた
　　（どう出すのかわかんなくなってきた）

事例：自動販売機
　商品を選ぶ
　お金払う
　キャンセルできる

要求に変える

立ち上げる
プロジェクト作成
マシン作成
コンテキスト作成
Open WithでRodin Editorで立ち上げる
上にウィザードがある
それに埋めていく形でつくる・・・

・・・りーなすせんせい、スパルタです
わたしは、ついていけなくなりました・・・・（；＿；！）

リファインメント
　データ構造の追加
　抽象モデル

元のモデルの右ボタンで
　Refine
OpenWidthでRodin Editorに変える

・・・また、ついていけなくなりました。

---

■Alexei先生
Rodinエコシステム
　拡張できる・変更可能
Open Rodin プラットフォーム
　だれでもエクステンションできる（プラグインで）

プラグイン
　モデリング
　　　UML-B　グラフィカルなフロントエンド
　検証
　　　atrlier-B
　　　ProB
　ユーザビリティ
　　　エディタ、アニメーション、チームワーク
　モデルチェック
　　　Prob,AnimB
　コード生成・モデルインポート／エクスポート

Decomposition
　変数をシェア
　エベントをシェア

ユースケース
　　Flowプラグイン

ProB
　　LTLのチェッキング

UML-B
　ステートマシンで
　　　http://wiki.event-b.org/index.php/Rodin_Plug-ins

EventBの本

メーリングリストさかん

Flowプラグイン
　　relation
Disable
　　　Feasibility
図を描いて実演！！
　　http://wiki.event-b.org/index.php/Flows

---

■エレナ先生

Event-B高信頼性システム

ディペンダビリティエンジニアリングとフォーマルモデリング

例
　　Lynaデザインシステム
　　　コントロールフロー
　　　　　サービスは、ワンバイワンで

フォールトトレラントの評価

Probabilistic モデリング：intuition
　　抽象モデル
　　　result OKかno
　　Probabilistic モデリング
　　　result OKがp noが１－ｐ
ProbabilisticなB
PRISM：Probabilisticな検証

セイフティ分析
　　FEMA
　　FTA
　　　→セイフティ要求（ゴール）
　　　　ハザードの確率の計算

フォーマルモデルからセイフティケース
ゴール→戦略→議論
　 26262

要求→フォーマルメソッドに→セイフティケース
　　　　　変数
　　　　　不変条件

EventBからセイフティケース

---

■ロマノフキー先生

サクセスストーリー
　FP6　RODIN
　FP7　DEPLOY
　あふたーDEPLOY
　FP7　ADVANCE

DEPLOY　
　ボッシュ
　シーメンス
　スペースシステム（フィンランド）
　SAP（BPMN)

---

■しゅくだい
　３問のうち、１番目を明日まで

ソフトウェア業界は「貧乏暇なし」っていうのが実態？

昨日の、

ソフトウェア業界は、アベノミクスの恩恵を受けていない。その証拠
http://blog.goo.ne.jp/xmldtp/e/6a008688e19dc3fa20b5e4b6df1dc5dc

はちょっと意外かもしれない。いや、体感的には、仕事は増えている
ように感じるからだ。人は逼迫してないか？

---

■「プロジェクトの炎上が増えた」では説明できない


ということで、ありえる可能性をさぐってみる。
今の状態は要するに、

　　　売上は増えていないけど、仕事量が増えている

ときいてすぐに考えられるのは、「プロジェクトの炎上」
といっても、ツイートが増えるという意味ではなく（＾＾；）
プロジェクトがデスマーチになり、残業では間に合わず、
新規人員を投入しているんだけど、お客さんに請求できない
（売上は増えない）ケース。

　ただ、今も昔も、デスマーチは変わらないだろう。
　アベノミクスになってから、そうなったと考えるのは不自然なので
この要因もあるかもしれないけど、他に要因はありそう。

---

■その他、説明できないこと、あれこれ

　もう一つは、売上が立つ時期と仕事が増える時期の不一致。
　工事完成基準を採用すると、ソフトが出来てから売上が発生
するので、まず、人が働いて（このとき人が逼迫する）、それから
景気が良くなるはずという考え方。

　しかし、現在は、工事進行基準をとっているので、この考えは
ないと思う。

　また、予算がついてから開発にはいるので、アベノミクスの効果は、
景気が良くなり、企業に余裕が出来て、予算が付いてから出るという
考えも成り立つが、これは、人が逼迫している理由を説明できない。

---

■説明できるストーリー：単価が下がった

はじめの命題に戻ろう。

　　　売上は増えていないけど、仕事量が増えている

状況は、どういうときがありえるか。

　売上　＝　仕事量　X　単価

なので、単価が下がれば、仕事量が増えても、一定になる
単価が下がる要因はあるか？ある・・・・

---

■仮説１：スマホブームが単価を下げた

急成長するスマホアプリ市場、2012年は140億円規模に
http://www.itmedia.co.jp/promobile/articles/1203/27/news082.html

なんていう予測記事を出さなくても、スマホアプリが増えていることはわかる。
で、スマホアプリ開発は、

イマドキの１人月単価は、いくらが妥当なのか？
http://blog.goo.ne.jp/xmldtp/e/ecea12c3aa49fe1a325568da8d330221

にはっきり書いていないけど、実は、１人月単価が安い。
そこで紹介したサイト
（https://mcea.jp/anken-tokyo）
で見てもらうと分けるけど、スマホ開発は、１人月
７０～５０万、ってことは平均６０万円台くらい。
普通の開発は、８０～６０万、平均７０万くらいになるはず

ということは、スマホアプリ開発が増えると、平均１人月単価も減る。
なので、それにつられて、全体的に１人月単価が減るというストーリーも
なりたつ。

---

■仮説２：ソフトウェア産業の売上は開発量で決定するわけではない

そもそも、ソフトウェア産業の売上は、開発量できまるのではなく、
年初の予算で決まる。
もちろん、スマホアプリなどはそうではないが、スマホアプリ売上は、
ソフトウエア産業の売上全体から見ると、そんなに大きくはない。
ソフトウエア産業の売上全体を左右する大きな開発は、年間予算で確保
される。ので、アベノミクスの効果はまだでない。

結果として、売上は増えないが、スマホ開発などが増えて、全体の開発量
は増えている。単価も安くなっているので、

売上（一定）＝仕事量↑　X　単価↓

という構図になっているのではないかと思われる

---

要するに、単価が減って貧乏になってるけど、
仕事量が増えて暇なし
「貧乏暇なし」っていうのが実態？