中島震の作品一覧
「中島震」の「Event-B：リファインメント・モデリングに基づく形式手法」「SPIN モデル検査：検証モデリング技法」ほか、ユーザーレビューをお届けします！
- 作者をフォローする
- フォローすると、この作者の新刊が配信された際に、お知らせします。
作品一覧
-
SPIN モデル検査：検証モデリング技法
ビジネス・実用
4.01巻4,180円 (税込)※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。 社会の様々なところにソフトウェアが組み込まれる中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況にある。そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。本書はSPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍である。 -
Event-B：リファインメント・モデリングに基づく形式手法
ビジネス・実用
-1巻4,180円 (税込)※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。 論理的なバクを発生させない形式手法!!Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。 -
Bメソッドによる形式仕様記述
ビジネス・実用
5.01巻3,960円 (税込)※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。 仕様の段階で誤りをなくす注目の手法「Bメソッド」を実践活用するための解説書。安心安全を含めてますます高度な機能や性能が要求されるソフトウェアシステムの開発において、厳密な仕様記述を基に開発を行う形式手法に対する関心と期待が高まっている。本書は、我が国初のBメソッドの書き下ろし入門書である。実際の開発への適用を意識した実用指向の内容が、平明でわかりやすく記述されている。 -
デジタル・プラットフォーム解体新書 製造業のイノベーションに向けて
ビジネス・実用
4.01巻2,750円 (税込)※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。 イノベーションを解き明かす！ インターネットを基盤とした情報技術が、あらゆる分野の産業に新しいイノベーションを起こしている。本書は、これらの背景を歴史的変遷と技術的変遷の両方から紹介する。特にその中核となるデジタル・イノベーションやデジタルプラットフォームについては、単なる技術の視点だけでなくビジネスと技術の両面から本質を解き明かしており、また、イノベーション・モデルの転換やプラットフォームの役割についても、技術基盤としてのソフトウェアとビジネス思想としてのオープン＆クローズ戦略という、2つの視点から解説する。ドイツのインダストリー4.0をはじめとする各国の動きにも触れており、産業政策などに関心のある読者にとって有意義な1冊である。
ユーザーレビュー
-
-
Posted by ブクログ
▪️サービス化
"As a service"と呼ばれるビジネスモデルでは、メーカーが機器をアセットとして保有し、ユーザーに貸し出す。ユーザーは初期投資を削減できる。メーカーは機器の所有権を保有しているため、ソフトウェアのアップデートや機器からの情報収集を容易に行える。一例として、KUKAは"Robot as a serviceというビジネスモデルを採用している。
GEは、aviation事業とエネルギー事業において、機器を提供するメーカーと機器を運用する企業という従来の取引関係を超えて、事業領域を運用企業側の保守・運用に広げた。ほかに下位の機器メーカーであったBoschは、最終製品メーカーを越えてエンドユーザーにサービスを提供するようになった。『アフターデジタル』で、顧客接点を持たないメーカーはサービス提供企業の下請けになってしまうと述べられていたことに対する、一つの答えかもしれない。
コマツはサービス化を行いながらも、メーカーとしてのアイデンティティを変えていない。従来からの製品である建機のコア技術（キーコンポーネント技術）を中心に据えている。
▪️プラットフォーム化
プラットフォームを構築し、それぞれの得意分野に応じた外部リソースをプラットフォームに提供してもらう（アウトサイド・インによるオープン・イノベーション）。これにより、多様なサービスの提供が可能になり、範囲の経済を達成することができる。加えて、魅力的なプラットフォームを形成すれば、ユーザーが増えて、規模の経済を達成することができる。
両面プラットフォームモデルにより両面市場 (two-sided market) を構築することのメリットは、多様な顧客ニーズに応えられること、新たな収益機会が創出されること、取引に関するデータを入手できることである。ただし、B2B分野で可能であるのかは検証が必要である。例えばコマツは、建機などのデバイス提供者、そのユーザー、ユーザーにサービスを提供する企業などを結び付ける両面プラットフォームモデルを構築した。ほかに、Siemensの産業用オープンIoT基盤「MindSphere」やGEの産業用オープンIoT基盤「Predix」が両面プラットフォームモデルの例である。
▪️知財戦略
自社のコア領域だけでなく、開発支援、導入補助、運用保守などの周辺領域や、コア領域を含めたアーキテクチャを特許化することが重要である。この考え方は参考にしたい。 -
Posted by ブクログ
初心者向けSPINの実用書です。
SPINとは、"Simple Promela Interpreter"の略で、"Promela"は、Gerard J. Holzmannが作った並列処理を伴う状態遷移（オートマトン）を記述できる形式仕様記述言語のことです。
この本は、実例（Promelaプログラムサンプル）を通してソフトウェアの振る舞いの形式記述法を学び、SPINでそれを動かしてデッドロックや、プロセスのプライオリティ逆転等々のモデルチェッキングの方法を学ぶことができます。
SPIN自体は、プログラマが振る舞いの検証を行うために使うツールと思いますので、いわゆる第三者検証を実施しているテスト設計を行う人が使うことはないと思いますが、SPINでどんなことが検証できるのかを知っておくことは悪くないと思います。
また、特に9章の「検査対象の大きさを適切に保つ……抽象化の方法」は普通のテスト設計にも非常に役に立つと思います。この章の始めに、抽象化が重要であることは容易にわかるが、抽象化によってシステムがもともと持っていた性質が消えてしまっては元も子もない。という文があるのですが、じゃあどういう観点で抽象化していくのと言う答えがこの章にあります。節名だけ書くと、
9.2 データ値に着目した抽象化
9.3 制御の流れに着目した抽象化
9.4 連続時間の抽象化
です。
山本訓稔さんがリーディングされている「Model Checkingを適用した実践的非同期制御検証」は、要するにモデル設計フェーズで作成しているxUMLからPromelaを自動生成するツールを作ったってことです。
こうすることで、xUMLからC++へ変換されるC++の3万行のコードに対して、300万もの状態を自動検証したことと同等の効果を得ることができ、きわどい欠陥を検出できています。
つまり実用段階の技術となってきているのですね。
