第73回 SEA関西プロセス分科会「モデルベースシステムズエンジニアリングの活用」の感想～モデルの検証を形式手法で自動テスト化する

第73回 SEA関西プロセス分科会「モデルベースシステムズエンジニアリングの活用」の感想をラフなメモ書き。
適当なメモ。

あくまでも僕の理解なので、論理が端追っていたり、論理が飛んでいる。

【参考】
モデルベースシステムズエンジニアリングの活用 - connpass

第73回 SEA関西プロセス分科会 「モデルベースシステムズエンジニアリングの活用」 の見所 #seakansai: プログラマの思索

【1】高井さんの2つの講演「モデルベースシステムズエンジニアリングにおける形式手法の効果的な活用」「モデルベースシステムズエンジニアリングにおけるシナリオ生成手法の効果的な活用」は共に、SysMLと戦略の観点のマトリクスによるモデルから、形式手法などのツールを駆使して、別のモデルを作り出し、その生成技法をastahのプラグインで実装したというお話。

あまり詳しくなければ、昔流行したMDA（モデル駆動開発）とか、超高速開発のようなツールを連想してしまうが、実際に聞いてみると、こういうものを実装したい時代背景や動機が色濃くあることがよく分かった。

実際、高井さんが、モデリング技法（astahなどのモデリングツール）と各種の技法（形式手法Spinなど）がほどよく洗練されてきたので、使いやすくなった、と言っていた。

たとえば、形式手法のSpinの問題点は2つあるが、問題点を薄めやすいという。
一つは状態爆発しやすいことだが、状態遷移図だけでなく、SysMLでは上流工程の要求モデルや他のモデルの情報をもとに、状態遷移を明確にすることで、状態爆発しない程度までに抑えることができる。
もう一つは、Spinで検査式が難しくて書きにくいことだが、SysMLのダイアグラムに制約条件を書き込んだり、他ツールとのトレーサビリティから情報を集めて、検査式を作りやすい。

つまり、モデルベースエンジニアリングによるモデルには豊富な情報が含まれているので、形式手法のSpinに合うような情報を連携すれば、Spinの弱点を解決でき、Spinのプログラムを自動生成できるようになるわけだ。

【1-1】具体的には、上流工程から下流工程までの各種のモデルを生み出す技法と、形式手法を組み合わせて、モデルそのものの検証が行えること。
つまり、モデルをいくら書いても、そのモデル自体の正しさはそのままでは保証できないが、モデルに描かれた仕様や制約条件を元に、形式手法のプログラムへ自動生成できれば、モデルそのものを検証できる。
さらに、モデルのテストケースもSysMLで書いておけば、テストケースそのものも形式手法プログラムの一つになる。

デモでは、モデルから形式手法プログラムへの自動生成とモデルの検証をastahで行い、モデルの検証結果がOKであれば、astah上のテストケースが緑色、検証結果がNGなら赤色に変わるように反映されていた。

この手法を使えば、astahで描かれたモデルの検証ケースをテストケースで全て書き込んでおいて、継続手インテグレーションで回せば、モデル検証を自動テストできる仕組みが構築できる。
そうすれば、上流工程のモデルを修正したり追加するたびに、自動テストを動かして、モデルの整合性や正しさを保証できるように運用できるはずだ。

本来は、astahのモデルではなく、PlantUMLのように、モデルをソースコードで書くようにできれば、SpinやLTSAのような形式手法プログラムでモデル検証の自動テストがやりやすくなるはずだ。

【1-2】あるいは、具体的には、自動運転の自動車部品のセキュリティ対処の為に、セキュリティの穴をつくような攻撃シナリオや防御シナリオをastahのGSNモデルとして描き、そこから、具体的に設計や実装が可能なシナリオを自動生成すること。
おそらく、astahGSNで、自動車部品のセキュリティのシナリオを論理的に書いておき、そこからパターンごとにシナリオを生成するイメージ、かな、と思った。
すると、シナリオを元に、具体的な仕様モデルや実装モデルを設計できる。

なお、Spinのような形式手法プログラムもコマンドライン・ベースで動くので、astahの画面からキックして、Spinプログラムを実行できたり、ログ出力された実行結果を読み取ることができる。
Spinはもう随分枯れた形式手法だが、プログラムのI/Fはコマンドラインのまま古い点が逆に良い点に作用しているのだろう。

そういう話を聞くと、astahは外部から接続できるAPIが公開できていたり、astahのプラグイン実装が可能な点が有効に活用できているのだろうと思う。

個人的には、PlantUMLのようにUMLやSysMLをソースコードで書いて、SpinやLTSAのような形式手法プログラムを自動生成＆自動テストを実行できる仕組みを作っておき、一方で、ソースコードで書かれたモデルはastahのようなビジュアルなモデリングツールにいつでも読み込めるようにする手法が運用しやすいのでは、と思う。
モデルがソースコードに落ちていれば、Gitで構成管理しやすいし、I/Fがコマンドラインで実行できるならば、形式手法以外の技法のツールと連携しやすいからだ。

【2】一番興味深かったのは、とある大学の先生の話。

フォルクスワーゲンは「ソフトウェアファースト」を掲げて製造業からソフトウェア業へ本当に変革しようとしていて、実際、2020年には2000～3000人ものソフトウェア技術者をドイツで募集しており、社員の割合もハード技術者とソフト技術者の割合が半々まで来ているらしい。

一方、トヨタも2020年になって社長自ら「ソフトウェアファースト」を掲げて、ソフトウェア技術者を応募しているが、今までのエンジン技術の成功体験もあって、そこまでソフトウェア重視ではないですね、とのこと。

僕は、DXとは、ITが中核事業でない既存企業がソフトウェアを中核とした事業にシフトすること、と思っているので、日本企業がソフトウェアにまだまだ詳しくないからこそ、DXというバズワードが流行しているんだろうな、とか思った。

つまり、DXとは、従来の事業スタイルのメーカーや小売業が、新興勢力のソフトウェア企業に「代替品の脅威」を感じて、何とか自社でもソフトウェアを前提とした事業を打ち出そうと頑張るためのバズワード、と思っている。

すなわち。「DXとは、ソフトウェアが世界を食う脅威に従来型企業が怯えて対抗しようとしている活動」ではないか。

「ソフトウェアが世界を飲み込む理由」「ソフトウエア、それが問題だ」の記事のメモ: プログラマの思索

ソフトウェアが世界を動かす時代: プログラマの思索

VWがソフトウエア部門を一新、自社開発を大幅に増やす | 日経クロステック（xTECH）

「ソフトウェアファースト」で社会の一部となるクルマづくりへ、トヨタとNTT - MONOist（モノイスト）

【追記】
当日の講演資料が公開されました。