VDM++によるオブジェクト指向システムの高品質設計と検証 ― 2010年07月29日 05時32分31秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特別セミナー
で書いた続き。
形式仕様記述(フォーマルメソッド、Formal Methods)関係の新刊が出ます。
翔泳社の古田島さん(コタさん)。
大して数が出ないだろうし、儲からないだろうから、社内で肩身が狭いかも
しれないが、こういう大切な本を出してくれて、ありがとうございます。
http://iiyu.asablo.jp/blog/2008/07/04/3609430
翔泳社 IT Architects’Archiveシリーズ
で書いたように、がんばって、出してくれてるんですよね。このシリーズは、
たぶん、ほぼ全てコタさんが手がけたものだろうと思います。
さて、本題の新刊というのが、
http://www.amazon.co.jp/exec/obidos/ASIN/479811961X/showshotcorne-22/
VDM++によるオブジェクト指向システムの高品質設計と検証 [大型本]
ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカ
ージー、ニコ・プラット、マーセル・バーホフ (著), 酒匂 寛 (翻訳)
コタさん、献本、ありがとうございます。
翔泳社にあるページは、
http://www.seshop.com/product/detail/12267/
VDM++によるオブジェクト指向システムの高品質設計と検証
送られてきた本書をみると、なんと、オビに九州大学の荒木啓二郎先生のお
言葉が。しかも、巻頭に荒木先生の推薦文が。
今度、九大に行くときに持っていって、荒木先生にサインしてもらおうかな。\(^O^)/
内容は、目次をみれば想像がつくと思うが、フォーマルメソッドでモデル化
する意義、VDM++やツールの解説、設計やモデリングの実際、モデルからJava
による実装まで、フォーマルメソッドを実際に適用するとは、どういうものか
を、わかりやすく解説したもの。
ケーススタディで、おおっと思ったのが、第2次世界大戦中、ドイツが誇っ
た超強力暗号エニグマの例。エニグマ暗号機をVDM++でモデル化するの。
エニグマのロータやプラグボードもモデル化している。エニグマを知らない
人のために、歴史などの解説があって、チューリングたちが解読したこと、世
界最初のプログラム可能な電子式コンピュータの1つであるコロッサス
(Colossus)のこと、チャーチルが秘密を守るためにコロッサスを解体し、情報
封鎖したために、ENIACより先に稼働していたのに、長らく世界最初のプログ
ラム可能な電子計算機だということが世界に知られてなかったことなどなどが
出てくる。
脱線するが、エニグマにまつわるこの辺の話を含め、暗号の歴史を知るには、
それもわくわくする筆致で詳しく知るには、
http://iiyu.asablo.jp/blog/2008/12/22/4020425
楕円曲線、暗号といえば
をはじめ、何度も紹介している、
http://www.amazon.co.jp/exec/obidos/ASIN/410215972X/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 上巻 (新潮文庫 シ 37-2)」
http://www.amazon.co.jp/exec/obidos/ASIN/4102159738/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 下巻 (新潮文庫 シ 37-3)」
がお薦め。
さてさて、フォーマルメソッド、VDM++といえば、最大、最高の成功事例は、
フェリカネットワークスの事例。
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
で、
http://techon.nikkeibp.co.jp/article/HONSHI/20051213/111568/
日経エレクトロニクス2005年12月19日号
特集「ソフトウェアは硬い」
に出ているフォーマルメソッドの記事の中でも、
--- ここから ---
フェリカネットワークスの事例がインパクトがありまくり。ここは、モバイル
FeliCa、つまり、EdyとかSuicaとかおサイフケータイなどをやっている会社で
す。
--- ここまで ---
と書いたが、この前、九大に行ったときに、荒木先生から聞いた話では、
FeliCaの事例は、おれだけじゃなくて、世界的にもインパクトがありまくりで、
国際会議をはじめ、あちこちから講演してくれという話が多いらしい。
フェリカネットワークスの人たちは、本書で解説してある形式仕様記述言語
VDM++で、10万行も書いたんだから、すごいよね。しかも、仕様の段階で350件
ほどのバグを潰している。
そして、ほんとにすごいのは、FeliCaのチップは、Edy, Suicaをはじめいろ
んなところで、去年の段階で1億数千万枚使われているらしいが、これまでチ
ップにはバグが1つもないこと。
これだけ広く社会に使われているもので、バグが1つもないなんて、ほとん
ど奇跡にしか思えないわけで、ギネスブックに申請しようかという話があるく
らいだそうだ。
おれがみるところ、成功の要因は、単にVDM++を使ったからよかったなどと
いう話ではない。
もちろん、フェリカネットワークスの人たちが優秀ということもあるだろう
が、開発プロセス全体をちゃんと見直して、再構築している。
つまりですね。現場の優秀さだけじゃなくて、経営者、経営層がバカだと、
こうはならないんですよ。経営者、経営層の理解があって、こういうことに投
資できないと成功しないわけ。
http://ci.nii.ac.jp/naid/40017084078
経営者はアーキテクチャと形式手法を忘れてはいけない
藤枝純教
という論文もあるくらい。
フェリカネットワークスの栗田太郎さんの論文が読めますね。
http://www.ipsj.or.jp/15dp/Vol1/No3/IPSJ-DP0103007.pdf
モバイル FeliCa のソフトウェア開発における品質確保のための構造と実践
フェリカネットワークス 栗田太郎
このあと、フォーマルメソッドに関する日本語の教科書のリストを書く。
追記:書いた。
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書
関連:
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
http://iiyu.asablo.jp/blog/2008/08/04/3672175
形式的仕様記述の国際会議ICFEM2008
http://iiyu.asablo.jp/blog/2007/08/06/1708469
仕様記述言語Zのテーマソングが決定
http://iiyu.asablo.jp/blog/2008/09/20/3775398
Eiffel, 仕様記述(フォーマルメソッド)
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特別セミナー
で書いた続き。
形式仕様記述(フォーマルメソッド、Formal Methods)関係の新刊が出ます。
翔泳社の古田島さん(コタさん)。
大して数が出ないだろうし、儲からないだろうから、社内で肩身が狭いかも
しれないが、こういう大切な本を出してくれて、ありがとうございます。
http://iiyu.asablo.jp/blog/2008/07/04/3609430
翔泳社 IT Architects’Archiveシリーズ
で書いたように、がんばって、出してくれてるんですよね。このシリーズは、
たぶん、ほぼ全てコタさんが手がけたものだろうと思います。
さて、本題の新刊というのが、
http://www.amazon.co.jp/exec/obidos/ASIN/479811961X/showshotcorne-22/
VDM++によるオブジェクト指向システムの高品質設計と検証 [大型本]
ジョン・フィッツジェラルド、ピーター・ゴルム・ラーセン、ポール・マッカ
ージー、ニコ・プラット、マーセル・バーホフ (著), 酒匂 寛 (翻訳)
コタさん、献本、ありがとうございます。
翔泳社にあるページは、
http://www.seshop.com/product/detail/12267/
VDM++によるオブジェクト指向システムの高品質設計と検証
送られてきた本書をみると、なんと、オビに九州大学の荒木啓二郎先生のお
言葉が。しかも、巻頭に荒木先生の推薦文が。
今度、九大に行くときに持っていって、荒木先生にサインしてもらおうかな。\(^O^)/
内容は、目次をみれば想像がつくと思うが、フォーマルメソッドでモデル化
する意義、VDM++やツールの解説、設計やモデリングの実際、モデルからJava
による実装まで、フォーマルメソッドを実際に適用するとは、どういうものか
を、わかりやすく解説したもの。
ケーススタディで、おおっと思ったのが、第2次世界大戦中、ドイツが誇っ
た超強力暗号エニグマの例。エニグマ暗号機をVDM++でモデル化するの。
エニグマのロータやプラグボードもモデル化している。エニグマを知らない
人のために、歴史などの解説があって、チューリングたちが解読したこと、世
界最初のプログラム可能な電子式コンピュータの1つであるコロッサス
(Colossus)のこと、チャーチルが秘密を守るためにコロッサスを解体し、情報
封鎖したために、ENIACより先に稼働していたのに、長らく世界最初のプログ
ラム可能な電子計算機だということが世界に知られてなかったことなどなどが
出てくる。
脱線するが、エニグマにまつわるこの辺の話を含め、暗号の歴史を知るには、
それもわくわくする筆致で詳しく知るには、
http://iiyu.asablo.jp/blog/2008/12/22/4020425
楕円曲線、暗号といえば
をはじめ、何度も紹介している、
http://www.amazon.co.jp/exec/obidos/ASIN/410215972X/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 上巻 (新潮文庫 シ 37-2)」
http://www.amazon.co.jp/exec/obidos/ASIN/4102159738/showshotcorne-22/
サイモン・シン著, 青木薫訳「暗号解読 下巻 (新潮文庫 シ 37-3)」
がお薦め。
さてさて、フォーマルメソッド、VDM++といえば、最大、最高の成功事例は、
フェリカネットワークスの事例。
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
で、
http://techon.nikkeibp.co.jp/article/HONSHI/20051213/111568/
日経エレクトロニクス2005年12月19日号
特集「ソフトウェアは硬い」
に出ているフォーマルメソッドの記事の中でも、
--- ここから ---
フェリカネットワークスの事例がインパクトがありまくり。ここは、モバイル
FeliCa、つまり、EdyとかSuicaとかおサイフケータイなどをやっている会社で
す。
--- ここまで ---
と書いたが、この前、九大に行ったときに、荒木先生から聞いた話では、
FeliCaの事例は、おれだけじゃなくて、世界的にもインパクトがありまくりで、
国際会議をはじめ、あちこちから講演してくれという話が多いらしい。
フェリカネットワークスの人たちは、本書で解説してある形式仕様記述言語
VDM++で、10万行も書いたんだから、すごいよね。しかも、仕様の段階で350件
ほどのバグを潰している。
そして、ほんとにすごいのは、FeliCaのチップは、Edy, Suicaをはじめいろ
んなところで、去年の段階で1億数千万枚使われているらしいが、これまでチ
ップにはバグが1つもないこと。
これだけ広く社会に使われているもので、バグが1つもないなんて、ほとん
ど奇跡にしか思えないわけで、ギネスブックに申請しようかという話があるく
らいだそうだ。
おれがみるところ、成功の要因は、単にVDM++を使ったからよかったなどと
いう話ではない。
もちろん、フェリカネットワークスの人たちが優秀ということもあるだろう
が、開発プロセス全体をちゃんと見直して、再構築している。
つまりですね。現場の優秀さだけじゃなくて、経営者、経営層がバカだと、
こうはならないんですよ。経営者、経営層の理解があって、こういうことに投
資できないと成功しないわけ。
http://ci.nii.ac.jp/naid/40017084078
経営者はアーキテクチャと形式手法を忘れてはいけない
藤枝純教
という論文もあるくらい。
フェリカネットワークスの栗田太郎さんの論文が読めますね。
http://www.ipsj.or.jp/15dp/Vol1/No3/IPSJ-DP0103007.pdf
モバイル FeliCa のソフトウェア開発における品質確保のための構造と実践
フェリカネットワークス 栗田太郎
このあと、フォーマルメソッドに関する日本語の教科書のリストを書く。
追記:書いた。
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書
関連:
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
http://iiyu.asablo.jp/blog/2005/08/30/57720
荒木先生の形式仕様記述の教科書
http://iiyu.asablo.jp/blog/2008/08/04/3672175
形式的仕様記述の国際会議ICFEM2008
http://iiyu.asablo.jp/blog/2007/08/06/1708469
仕様記述言語Zのテーマソングが決定
http://iiyu.asablo.jp/blog/2008/09/20/3775398
Eiffel, 仕様記述(フォーマルメソッド)
コメント
トラックバック
_ ホットコーナーの舞台裏 - 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
高品質高信頼ソフトウェア開発の特
---
http://iiyu.asablo.jp/blog/2010/07/29/5254538
高品質高信頼ソフトウェア開発の特
_ ホットコーナーの舞台裏 - 2010年07月29日 05時46分45秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
例によって、直前になってここに書く。すみません。
高品質高信
---
例によって、直前になってここに書く。すみません。
高品質高信
_ ホットコーナーの舞台裏 - 2010年08月02日 09時34分14秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/07/30/5256211
「Kindleの新モデルはWiFiや日本語表
---
http://iiyu.asablo.jp/blog/2010/07/30/5256211
「Kindleの新モデルはWiFiや日本語表
_ ホットコーナーの舞台裏 - 2010年08月10日 07時18分43秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
小惑星フクオカ、ナカス、キュウダイなどを探査し、サンプルリタ
---
小惑星フクオカ、ナカス、キュウダイなどを探査し、サンプルリタ
_ ホットコーナーの舞台裏 - 2010年09月18日 04時47分57秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2010/06/17/5167670
関数プログラミングの楽しみ
で名
---
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
---
オーム社のgolden_luckyさん(鹿野さん)のつぶやき。
http://twitter.com/bonota
_ ホットコーナーの舞台裏 - 2011年09月19日 08時43分58秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
日経ITproから来たメールに【文章が駄目ならシステムも駄目】があっ
---
日経ITproから来たメールに【文章が駄目ならシステムも駄目】があっ
_ ホットコーナーの舞台裏 - 2013年04月17日 04時49分27秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonからホットコーナー(http://www.asahi-net.or.jp/~ki4s-nkmr/ )に転載したものから。
---
http://iiyu.asablo.jp/blog/2013/04/10/6773298
ソフトウェア・テスト PRESS 総集編
---
http://iiyu.asablo.jp/blog/2013/04/10/6773298
ソフトウェア・テスト PRESS 総集編
_ ホットコーナー - 2018年10月30日 02時21分51秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonから。
---
世の中、まだ、テスト駆動開発(TDD)しか知らず、形式手法(フォーマルメソッド、Formal Methods)を知らない人が多い。
以前書いたけど
---
世の中、まだ、テスト駆動開発(TDD)しか知らず、形式手法(フォーマルメソッド、Formal Methods)を知らない人が多い。
以前書いたけど
_ ホットコーナー - 2019年05月16日 10時25分37秒
ASAHIネット(http://asahi-net.jp )のjouwa/salonから。
---
アベンジャーズのエンドゲームを観たんよ。
マーベルのヒーロー総出演だから、よく知らんヒーローが多かった。
でも、ドクタ
---
アベンジャーズのエンドゲームを観たんよ。
マーベルのヒーロー総出演だから、よく知らんヒーローが多かった。
でも、ドクタ
_ ホットコーナー - 2021年02月01日 09時14分02秒
ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
お買い上げありがとうございます。
形式手法(フォーマルメソッド、形式仕様
---
お買い上げありがとうございます。
形式手法(フォーマルメソッド、形式仕様
_ ホットコーナー - 2021年09月29日 11時34分20秒
ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
もう早く書かないから、明日まで。
翔泳社が電子書籍を50%ポイント還元セール
---
もう早く書かないから、明日まで。
翔泳社が電子書籍を50%ポイント還元セール
コメントをどうぞ
※メールアドレスとURLの入力は必須ではありません。 入力されたメールアドレスは記事に反映されず、ブログの管理者のみが参照できます。
※なお、送られたコメントはブログの管理者が確認するまで公開されません。
※投稿には管理者が設定した質問に答える必要があります。