中島震のレビュー一覧

Bメソッドによる形式仕様記述

本位田真一 / 中島震 / 来間啓伸

抽象機械、変数の宣言、不変条件の宣言、変数の初期化、操作の定義、一般化代入の紹介がある。
抽象機械の整合性の検証として、最弱事前条件、不変条件の無矛盾性、初期化の整合性について説明がある。
集合論的に厳密に記述していくのがミソのようです。
Refinementという段階的詳細化をしていって実装までたどり着きます。各段階間の整合性を確認することによって、実装が抽象的に検討した性格を保っていることを保証します。
トップエスイー講座は受けにいけませんでした。

読者である北海道立工業試験場の堀さんに２度講習会を開いていただきました。

デジタル・プラットフォーム解体新書 製造業のイノベーションに向けて

高梨千賀子 / 福本勲 / 中島震

▪️サービス化
"As a service"と呼ばれるビジネスモデルでは、メーカーが機器をアセットとして保有し、ユーザーに貸し出す。ユーザーは初期投資を削減できる。メーカーは機器の所有権を保有しているため、ソフトウェアのアップデートや機器からの情報収集を容易に行える。一例として、KUKAは"Robot as a serviceというビジネスモデルを採用している。

GEは、aviation事業とエネルギー事業において、機器を提供するメーカーと機器を運用する企業という従来の取引関係を超えて、事業領域を運用企業側の保守・運用に広げた。ほかに下位の機器メーカーであったBoschは、最終製品メーカーを越えてエンドユーザーにサービスを提供するようになった。『アフターデジタル』で、顧客接点を持たないメーカーはサービス提供企業の下請けになってしまうと述べられていたことに対する、一つの答えかもしれない。

コマツはサービス化を行いながらも、メーカーとしてのアイデンティティを変えていない。従来からの製品である建機のコア技術（キーコンポーネント技術）を中心に据えている。

▪️プラットフォーム化
プラットフォームを構築し、それぞれの得意分野に応じた外部リソースをプラットフォームに提供してもらう（アウトサイド・インによるオープン・イノベーション）。これにより、多様なサービスの提供が可能になり、範囲の経済を達成することができる。加えて、魅力的なプラットフォームを形成すれば、ユーザーが増えて、規模の経済を達成することができる。

両面プラットフォームモデルにより両面市場 (two-sided market) を構築することのメリットは、多様な顧客ニーズに応えられること、新たな収益機会が創出されること、取引に関するデータを入手できることである。ただし、B2B分野で可能であるのかは検証が必要である。例えばコマツは、建機などのデバイス提供者、そのユーザー、ユーザーにサービスを提供する企業などを結び付ける両面プラットフォームモデルを構築した。ほかに、Siemensの産業用オープンIoT基盤「MindSphere」やGEの産業用オープンIoT基盤「Predix」が両面プラットフォームモデルの例である。

▪️知財戦略
自社のコア領域だけでなく、開発支援、導入補助、運用保守などの周辺領域や、コア領域を含めたアーキテクチャを特許化することが重要である。この考え方は参考にしたい。

SPIN モデル検査：検証モデリング技法

中島震

初心者向け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万もの状態を自動検証したことと同等の効果を得ることができ、きわどい欠陥を検出できています。

つまり実用段階の技術となってきているのですね。