今年のMODELS 2021、Industry Days
10月中旬、モデル駆動開発に関する国際会議 MODELS 2021（正式名称”24th International Conference on Model Driven Engineering Languages and Systems (MODELS)“）がオンライン開催されました。世界各国から研究者やエンジニア、経営者（マネージャー）など460名を超える参加者が集まり、キーノート、論文発表、ツールデモ、ワークショップやチュートリアルなど賑わいを見せていました。チェンジビジョンはブロンズスポンサーとしてカンファレンスを応援すると共に、Industry Daysでセッションを実施する機会を得ました。
Industry Daysセッションは産業界からの発表を集めた企画で、今年は5件の発表がありました。今回のブログでは、発表スライド（英語）をご紹介します。
※本ブログは英語で公開した投稿を元にしています。原文は英語ブログ”“Lightweight integration of MBSE and model-checking” Oct. 13, 2021@Industry Day, MODELS2021″をご覧ください。
“Light-weight integration of MBSE and model-checking”
チェンジビジョンからは “Light-weight integration of MBSE and model-checking”というタイトルで、高井がプレゼンテーションしました。
Abstract: Although model-checking is a powerful formal method with matured tools, there are some issues when applying it to industrial system developments, e.g. the state explosion problem, specifying verification formulas. On the other hand, industries facing difficulties in developing IoT, autonomous, or cyber-physical systems are trying to adopt model-based systems engineering(MBSE). In this presentation, we show possibilities that applying model-checking in the context of MBSE can cover up the issues of model-checking and enjoy the benefits of model-checking.
発表では、参加者とMBSEの背景を共有し、形式手法の一つであるモデル検査（※1）技術が包含する難しさについて述べました。続いて、両者をうまく融合させることで、期待するだけの良い成果を生み出せることを示しました。
※1：モデル検査は、システムのコンポーネントや部品ごとの様々な状態の組み合わせを全網羅探査し、検査式（守るべき性質）が満たされているか確認する検証手法です。車で例えると、ドアが開いている状態と車両が走っている状態は同時に起こってはならないので、これを前述の検査式で表現すれば、システムのすべての状態の組み合わせで起こりえないことを検査できます。
ケーススタディとして、自動車のサブシステムのMBSEでモデル検査アプローチを採用した例を示し、MBSEにおけるモデル検査が重要な役割を果たすことを紹介しています。
後半では、本研究をまとめて、MBSEとモデル検査／シミュレーションが今後推進すべき四つの方向性を提示しました。
- SysMLモデルを使って、モデル検査の検査式を記述する
- 検査式は、SysMLモデルから自動で取り出す
- モデル検査技術をリスク分析、ハザード分析と統合する
- 安全性論証を記述する際、モデル検査ツールの結果を活用する
プレゼンテーション終了後、参加者からはいくつかの質問が挙がり、有意義な意見交換ができたとのことでした。プレゼンテーションスライドはどなたでもダウンロードできますので、どうぞご覧になってみてください。
スライドで使用しているMBSEツール astah* System Safety
プレゼンテーションスライドに登場するSysMLの各図は、astah* System Safetyで作成されたものです。このツールはMBSEツールで、SysMLによるシステムズエンジニアリングの他、STAMP/STPAを使ったリスク分析、ハザード分析、GSN（Goal Structuring Notation：ゴール構造表記法）を用いた安全性論証にも活用できます。SysMLのモデル図を描いてみたい方、ツールに関心のある方など、どなたでも無料で40日間の試用が可能です。
astah in 5 min 