Google
ブログ(iiyu.asablo.jpの検索)
ホットコーナー内の検索
 でもASAHIネット(asahi-net.or.jp)全体の検索です。
 検索したい言葉のあとに、空白で区切ってki4s-nkmrを入れるといいかも。
 例 中村(show) ki4s-nkmr

ウェブ全体の検索

形式仕様記述(フォーマルメソッド、Formal Methods)2006年08月19日 23時05分10秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 2006/08/06の「純粋関数型言語Concurrent Clean」のときに、
「この前、九大に教えに行ったとき、Formal Methodsの我が国の第一人者であ
る荒木啓二郎先生から直接お話を聞いて、仕入れてきました。それは、次の機
会に。」
と書いたけど、怠けと忙しさと体調不良で遅れに遅れてすみません。
 もうすぐ
LL Ring
なので、その準備もあって、いくらなんでもその前に書いておかないと最後に
あるように、荒木先生の第3回九州組込みソフトウェア研究会(QUEST)
での講演すら終わっちゃうので、簡単ながら書いておきます。

 形式仕様記述(フォーマルメソッド、Formal Methods)は、ぼくらが学生だっ
た25年前でも盛んにやられていたんですけど、当時は実用じゃなくて、論
文向けに小さなプログラムでああだ、こうだという感じだったんです。
 でも、いま、PerlやRubyといった、30年前遅い遅いといわれたLispより、30
倍も100倍も遅いスクリプト言語が実用になる世の中になったでしょ(*1)。

*1
 Lispが遅いといわれたのは30年前。いまのLispは、時にCに匹敵するくらい速い。
 Perlが30倍遅くて、Rubyが100倍遅いというのは、あくまで個人的感覚。

 だから、フォーマルメソッドも実用になるんじゃないかなと漠然と感じてい
たわけです。
 で、九大に呼んでもらったフォーマルメソッドの第一人者の荒木先生とお話
ししていたら、最近、すごいんだよという話になって、
http://techon.nikkeibp.co.jp/article/HONSHI/20051213/111568/
日経エレクトロニクス2005年12月19日号
特集「ソフトウェアは硬い」
の抜き刷りをもらいました。
 これは、素晴らしい。雑誌で形式仕様記述のことをここまで詳しく、かつ、
わかりやすく書いてあるのは、初めてだろう。書いたのは、進藤智則記者です。
非常にいい仕事ですね。バグをなくすことに興味のある人は、ぜひ、一読して
ください。
 最近、すごいというのは、ものすごい実例が出てきているからです。
 特集の中にも出てきますが、ソニーのフェリカネットワークスの事例がイン
パクトがありまくり。ここは、モバイルFeliCa、つまり、EdyとかSuicaとかお
サイフケータイなどをやっている会社です。
 ここが、それまで自然言語やUMLで仕様記述をやってきてバグがつぶせない
ので、形式仕様記述言語VDM++で形式仕様記述を実践して大きな成果を挙げた
のです。すごいのが、VDM++で10万行も書いてること。\(^O^)/
 これで、実装前、すなわち仕様の段階で350件ほどのバグを潰してます。
 フェリカの技術者たちは、数ヵ月でマスターしてここまで使ったらしいです。
 荒木先生によれば、「彼らは、たしかに優秀だし、大学と違ってビジネスで
大金がかかっていて、本気でやるからすごい」とのこと。
 ケータイだと、バグで回収騒ぎになると、ソニーや松下、たしか、100億円
くらい損失出したりしましたよね。極論するとバグ1個で100億円飛ぶんだか
ら、そりゃ、必死になりますよね。
 バグ1個で数億円飛ぶとなると、技術者にフォーマルメソッドを使うように
仕向けてもペイするかななどと思っていたんですが、もっと少額でもペイしそ
うな気もします。
 この前、XMLで有名な檜山さんがアンテナハウスに来てくれて、講演してく
れたんだけど、檜山さんによれば、100億円とか、数億円なんて巨額じゃなく
ても、小さなウェブショップのソフトを作ってるような世界じゃ、バグでショ
ップが止まって、日銭で70万円や80万円などの損害が出ると、その世界じゃ、
かなり大変。だから、フォーマルメソッドって、もっと少額でも、どんどん広
まったほうがいいんじゃないかと。
 つまり、フェリカの場合は組み込みで、バグが出たら回収が大変という世界
だけど、ウェブはウェブで365日24時間運用になってきてるから、止まるとや
っぱ大変ということ。
 全面的にネットワークに依存しつつある世界では、もう、バグは致命傷にな
りかねない。それなのに、理論的なやり方じゃなくて、行き当りばったりでア
ドホックなことばっかりやってシステム開発ってやられてますよね。特に若い
ITベンチャーなんて、理論なんか知ってる奴はいないし、体力と安くこき使う
人海戦術だけで乗り切る戦法だから、破綻は目にみえてるわけです。
 形式仕様記述の登場背景、現状、ケーススタディやらは、前記、特集を読ん
でください。

 前置きが長くなったけど、形式仕様記述の入門書として荒木先生と張先生の
入門教科書を紹介します。

http://www.amazon.co.jp/exec/obidos/ASIN/4274132633/showshotcorne-22/ref=nosim
荒木啓二郎、張漢明著「プログラム仕様記述論」
です。
 実はこの本、おれ、出版されたときに送ってもらって、去年のいまごろ、紹
介しているんです。
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
をどうぞ。
 荒木先生たちが訳した
http://www.amazon.co.jp/exec/obidos/ASIN/4781907164/showshotcorne-22/ref=nosim
M.ヘネシー著「プログラミング言語の意味論入門」
も役立つかも。
 おれ、これ、たしか、当時、ゲラ、読ましてもらったんじゃないかな。ひょ
っとして、ゲラ、もらって帰ってきたかも。もし、そうだとしても、もう、ど
こにあるかわからんけど。^^;
 なお、この本、7月中旬に調べたとき、amazonのユーズドで12600円もして
いました。「184ページの本で、12600円はかなりのプレミアですね。^^;」と
荒木先生にメールしたくらい。今日(2006/08/19)現在は、2260円ですね。1万
円も安くなってる。\(^O^)/

 上記、教科書の内容は
http://dontaku.csce.kyushu-u.ac.jp/books/ProgramSpecification/
プログラム仕様記述論
でも公開されています。
 本と違って、公理や規則などポイントのみで、文章による説明はほとんどあ
りません。説明がほしいなら本でしょうね。逆にFlashのアニメーションを使
っているので動きがあってわかりやすい面はあります。特に部分的正当性の証
明は、Flashのアニメだとだんだん上に積みあがっていくので、本よりわかり
やすいと思います。
 だから、併用するのが一番ですね。
 その他
http://unit.aist.go.jp/cvs/tr-data/sympo/araki.pdf
システムモデル化と形式仕様記述
もどうぞ。参考文献が参考になるかも。

 荒木先生からは、ErlangとVDM++の話も伺ったんですが、その話というのは、
http://unit.aist.go.jp/cvs/tr-data/sympo/tokimatsu.pdf
「形式仕様記述言語VDM++による形式モデルの構築と関数型言語Erlang による
実行」
ですね。
 あと、コンピュータ将棋の話も教わって論文ちょっともらったんですが、こ
れはいつか暇があれば。

http://www.erlang.org/
Erlang言語

 で、ぼくが九大に行ったあと、SEA(ソフトウェア技術者協会)のシンポジウ
ムが熊本であったんです。
http://ss2006.kmt-iri.go.jp/SS2006-Call.txt
ソフトウェア・シンポジウム2006
2006年7月19日(水)~21日(金)
ウェルシティ熊本  http://welcity.net/
です。これをみてもらえれば、どういうことをやってるかはわかると思います。
 東京に戻ってすぐ、こういう紹介を書いていれば、熊本に話を聞きに行けた
人がいたかもしれないけど、ぼくが相変わらずトロくて、どうも、すみません。

 そして、これはもう形式仕様記述のことを書けと宇宙から言われているな
(爆)と思ったのが、7月下旬に出たばかりの日経サイエンス2006年9月号に、
「欠陥を見逃すな ソフトウエア設計検証ツール」と題して、仕様記述、設計
検証ツールの記事が出ていたこと。
 日経サイエンスのウェブに簡単な記事紹介があります。
http://www.nikkei-bookdirect.com/science/page/magazine/0609/software.html
欠陥を見逃すな ソフトウエア設計検証ツール
をどうぞ。
 書いているのは、MITのDaniel Jacksonです。
http://people.csail.mit.edu/dnj/
彼らが開発したAlloyというツールを紹介しています。
http://alloy.mit.edu/
 ZやVDMなどほかのツールも表で紹介してあります。

 今度、荒木先生が「第3回九州組込みソフトウェア研究会(QUEST)」
~高信頼性組込みソフトウェアについて~において、「形式手法に基づく高信
頼化組込みソフトウェア開発」という題目で講演されますね。短い時間なので
ほんの入門と思いますが。
http://www.isit.or.jp/
九州システム情報技術研究所(ISIT)
のウェブに行っても、まだ、案内が出てないみたい。どういうこと? 直接
ISITの担当じゃないってことなのか。ISITからのメールじゃ、2006/08/02に来
ているのに。だもんで、メール全文引用します。
 締め切りが8/23なのでほとんど余裕がないですが、まだ間に合うでしょう。

--- ここから ---
*********************************************************************

 「第3回九州組込みソフトウェア研究会(QUEST)」
  ~高信頼性組込みソフトウェアについて~


・日 時 平成18年8月30日(水) 講演会 15:00~17:55


                   交流会 18:00~19:30


・会 場 福岡システムLSI総合開発センター 2階 (会議室A/B)
      (福岡市早良区百道浜3丁目8番33号)
       


[主催者挨拶]  15:00~15:05 
      福田 晃
        九州大学大学院システム情報科学研究院(QUEST会長)


[招待講演]   15:05~16:05
     「宇宙機ソフトウェアの高信頼性化の現状と組込み分野への応用」


・講 師  片平 真史 氏 
         宇宙航空研究開発機構(JAXA)情報・計算工学センター


・内 容 
  宇宙分野のソフトウェア、特に人工衛星などの宇宙機に搭載する
 ソフトウェアの高信頼性化のために研究・利用されている技術を
 紹介するとともに、組込みソフトウェアへの応用について解説します。
  また、高信頼性のための設計技術や検証技術について事例を紹介すると
 ともに現在の技術適用時の注意点などを紹介いたします。


・プロフィール
  宇宙ステーション、ロケットなどの開発業務を得て、
  高信頼ソフトウェア開発保証及びソフトウェア安全性に関する業務に長年
従事。
  特に、プロセス改善、ソフトウェア独立検証及び妥当性確認(IV&V)、
  高信頼性RTOS開発に関する業務のチームリーダ。


  1987年     宇宙開発事業団(NASDA)入社
  1999年~2001年 マサチューセッツ工科大学 航空宇宙工学部 
  Complex Systems Research Lab(Prof. Nancy G. Leveson) 研究員・講師


[招待講演]   16:05~16:50
     「組込みソフトのテストについて」


・講 師  森 孝夫 氏
        三栄ハイテックス株式会社


・プロフィール
  元高校の数学教師という経歴を持つ、教育者型の組込みエンジニア。
  1996年、三栄ハイテックス(株)に入社。システム開発課に所属し、
  デバイス関連のソフトウェアテストを経験後、ソフトウェア、システム開

  に従事。一方で社内ソフトウェアの教育の立ち上げを推進、確立。
  現在は、プロセス改・ソフトウェア設計のコンサルティングに従事。

  SESSAME/TOPPERS会員
  情報処理学会正会員

・著 書 「組込みソフトウェア開発のための構造化モデリング」共著。



        <<< 休憩 >>>   16:50~17:05



[講 演] 17:05~17:30
     「Windows Embedded OSにおける高信頼化組込ソフトウェア開発」


・講 師  奥薗 啓朗 氏  
         安川情報システム(株) 組込コンポーネント事業本部


・プロフィール
  ハードウエア設計を経験したのち、ソフトウェア設計・開発に従事。
  一貫してハードウェア・ソフトウェアに関するEmbedded業務に携わる。
  現在、Microsoft社のEmbedded OSを中心とした、OS・デバイスドライバの
  ポーティング事業のマーケティング・営業管理に従事。


  1984年 東海大学工学部通信工学科卒業
  1984年 (株)日本デジタル研究所入社
  1988年 安川情報システム(株)入社


[講 演] 17:30~17:55
     「形式手法に基づく高信頼化組込みソフトウェア開発」


・講 師  荒木 啓二郎 氏  
         九州大学大学院システム情報科学研究院 教授


・プロフィール
  1978年 九州大学大学院修士課程修了
  1982年 工学博士(九州大学)
  1985年 訪問研究員(アメリカ合衆国イリノイ大学)
  1989年 文部省在外研究員(ドイツ連邦共和国パッサウ大学)
  1993年 奈良先端科学技術大学院大学 情報科学研究科教授
  1996年 九州大学大学院システム情報科学研究科情報工学専攻教授
  2000年 九州大学大学院システム情報科学研究院情報工学部門教授
  2004年~九州大学附属図書館副館長(兼)
  現在に至る


[交流会] 18:00~19:30
福岡システムLSI総合開発センター 4階 (交流サロン)

・対象者  どなたでもご参加いただけます。


・参加費  講演会参加費  無 料
     (ただし、交流会参加の方のみ2,000円(領収書を発行します)

      ISITの賛助会員の方は無料です。
    (http://www.isit.or.jp/kaiin.html 賛助会員一覧でご確認くださ
い)


・定 員  100名程度


・主 催  九州組込みソフトウェア研究会(QUEST)
      情報処理学会九州支部
      (情報処理学会九州支部の特別事業として行います)


・共 催  (財)九州システム情報技術研究所(ISIT)


・後 援  九州経済産業局(予定)
(財) 福岡県産業・科学技術振興財団(ふくおかIST)
      福岡市経済振興局産業政策部新産業課
(社) 組込みシステム技術協会九州支部
      電波新聞社


・申込み締切日  8月23日(水)


・申込方法 下記にお名前等をご記入のうえ、
       E-mail(koryu@isit.or.jp 宛)等でご返送ください。
       すべてのお申込みに対しご返事いたします。


  なお、過去にISITが開催した定期交流会・技術セミナー等に
  申込まれている方で、肩書き等の変更がない方は、企業・団体名、
  氏名のみで結構です。
----------------------------------------------------------------
 「第3回九州組込みソフトウェア研究会(QUEST)」
    ~高信頼性組込みソフトウェアについて~

申 込 先 E-mail to:koryu@isit.or.jp
開催日時 平成18年8月30日(水) 講演会 15:00~19:30

企業・団体名 :
部課・役職名 :
氏 名    :
郵便番号   :
住 所    :
TEL番号    :
FAX番号    :
E-mailアドレス:
※懇親会   :  出席 ・ 欠席 (いずれかを削除願います)
-----------------------------------------------------------------
【個人情報の利用目的】
  今後、(財)九州システム情報技術研究所が催すイベント等に関する情報

ご案内以外の目的で利用することはありません。
  なお、今後のご案内に関して、いずれかを削除願います。
     ( 必要 ・ 不要 )

 *交  通

・詳細はホームページのアクセス&地図をご覧ください。
 アクセス:下記URL参照 (福岡システムLSI総合開発センター)
         http://www.ist.or.jp/lsi/pg03_01.html

・申込み・問合せ先
  〒814-0001 福岡市早良区百道浜2丁目1-22-707
  (財)九州システム情報技術研究所 事業部 有吉 / 田中 / 牧野
  TEL  : 092-852-3451 
  FAX  : 092-852-3455
  E-mail: koryu@isit.or.jp
  ホームページ:http://www.isit.or.jp
--- ここまで ---

 またしても直前での案内になって申し訳ないけど、熊本のシンポジウムみた
いに、終わってから案内してないので、許してください。^^;
 ISITのウェブ、案内を探してあれこれやってたら、オープニングイベントで
ぼくが話したことが記録されてますね。
http://www.isit.or.jp/eventinf.html
にある
http://www.isit.or.jp/eventinf/open.html
合同オープニングイベントのご報告
です。平成8年6月10日だから、もう10年前なんだ。所属がまだソフトヴ
ィジョンだし。
 ほんと人生あっという間。
 いま、若い人。ほんと若いうちに必死になれること見つけて、悔いのないよ
うに必死になったほうがいいよ。
 あっという間に、おれみたいに、もう人生終わっちゃったになるよ。\(^O^)/
 技術者としては、ウェブ2.0なんて、腐れ頭のチンポとマンコとケツの穴が
騒いでるだけのウンコなことに時間を使うくらいなら、形式仕様記述を学んだ
ほうが、長く使えるものだし、スキルも上がるし、1兆倍いいです。
 だって、人間だもの。\(^O^)/

コメント

コメントをどうぞ

※メールアドレスとURLの入力は必須ではありません。 入力されたメールアドレスは記事に反映されず、ブログの管理者のみが参照できます。

※なお、送られたコメントはブログの管理者が確認するまで公開されません。

※投稿には管理者が設定した質問に答える必要があります。

名前:
メールアドレス:
URL:
次の質問に答えてください:
一富士、二鷹、三は? ひらがなで。

コメント:

トラックバック

_ ホットコーナーの舞台裏 - 2008年03月11日 22時43分18秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2008/03/09/2714548
Joe Armstrong著, 榊原一矢訳「プロ

_ ホットコーナーの舞台裏 - 2008年09月20日 06時12分02秒

ASAHIネット(http://www.asahi-net.or.jp)のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2007/03/17/1284884
オブジェクト指向入門 第2版再

_ ホットコーナーの舞台裏 - 2009年12月01日 10時00分30秒

ASAHIネット(http://www.asahi-net.or.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 今年ももう12月になっちゃったよ~。早く書かないと、今年

_ ホットコーナーの舞台裏 - 2010年04月23日 07時16分17秒

ASAHIネット(http://www.asahi-net.or.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://www.amazon.co.jp/exec/obidos/ASIN/4270005769/showshotcorne-22/
数字で世界

_ ホットコーナーの舞台裏 - 2010年07月29日 05時25分08秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 例によって、直前になってここに書く。すみません。
 高品質高信

_ ホットコーナーの舞台裏 - 2010年07月29日 05時34分24秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特

_ ホットコーナーの舞台裏 - 2010年07月29日 05時42分21秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特

_ ホットコーナーの舞台裏 - 2010年09月18日 04時47分56秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/06/17/5167670
関数プログラミングの楽しみ
で名

_ ホットコーナーの舞台裏 - 2011年02月04日 02時24分06秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 オーム社のgolden_luckyさん(鹿野さん)のつぶやき。
http://twitter.com/bonota

_ ホットコーナーの舞台裏 - 2011年09月19日 08時43分57秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 日経ITproから来たメールに【文章が駄目ならシステムも駄目】があっ

_ ホットコーナーの舞台裏 - 2011年12月28日 10時27分35秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 来年1月16日-17日に「形式手法導入パイロット教育コース」というの

_ ホットコーナーの舞台裏 - 2012年08月01日 10時24分37秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 お買い上げありがとうございます。
 こりゃ、また、難しそうな本

_ ホットコーナーの舞台裏 - 2013年04月10日 05時37分42秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
 お買い上げありがとうございます。
http://www.amazon.co.jp/exec/obidos/ASIN/4

_ ホットコーナー - 2018年10月30日 02時21分51秒

ASAHIネット(http://asahi-net.jp )のjouwa/salonから。
---
 世の中、まだ、テスト駆動開発(TDD)しか知らず、形式手法(フォーマルメソッド、Formal Methods)を知らない人が多い。
 以前書いたけど
Google
ブログ(iiyu.asablo.jpの検索)
ホットコーナー内の検索
 でもASAHIネット(asahi-net.or.jp)全体の検索です。
 検索したい言葉のあとに、空白で区切ってki4s-nkmrを入れるといいかも。
 例 中村(show) ki4s-nkmr

ウェブ全体の検索