組込みシステム開発における
発見困難な不具合を
システム設計段階で早期抽出！
Dynaspecは、不具合早期発見のためのモデル検査ツールです。
設計者が作成したモデル図を基に、簡単な操作で設計上の不具合を早期発見し、大幅な手戻りを未然に防ぐことができます。
Dynaspecなら、シミュレーションでは発見の難しい不具合も抽出することができます。
導入事例
某自動車製造メーカー（OEM）様
HV車の走行モード切替制御にモデル検査を導入し、シミュレーションでは再現が難しかった不具合の発生条件を特定
東日本旅客鉄道株式会社 様
踏切制御を行うリレー結線論理に形式検証・ モデル検査を適用し、制御論理の安全性を向上
JAXA宇宙航空研究開発機構(国研) 様
飛翔体に搭載する自律飛行安全システムの設計モデル内に”重大な不具合が存在しないこと” を証明
某自動車製造メーカー（OEM）様
ハイブリッド車の走行モード切替制御に形式検証・モデル検査を導入し、シミュレーションでは再現が難しかった不具合の発生条件を特定しました。
自動車の制御などに用いる組み込みソフトウェアでは、割り込み発生の微妙なタイミングで不具合が発生することがありますが、その再現や発生条件の特定が難しい、という問題があります。
仕様・設計時点で不具合を検出し、無くしておくことが望ましいのですが、複数の制御の組み合わせで機能を実現している複雑な制御も多く、コンセプト通りに制御仕様が書けているかのチェックも困難です。
モデル検査では様々なモードやイベントのタイミングの組み合わせを網羅的に検証できるため、潜在している設計ミスを確実に検出することができます。
モデルベース形式検証ツール Dynaspecとは
Dynaspecは、モデリングツールEnterprise Architect（以下EA）のアドインツールです。
モデル検査という仕様検証手法を利用して、アーキテクチャ設計を動的検証します。
アクティビティ図などのモデル図が正しく構築されているかを検証し、検証結果を可視化することで設計段階での不具合検出を助けます。
EAで作成したモデル図を基に、簡単な操作で設計上の不具合を見つけだし、大幅な手戻りを未然に防ぐことができます。
モデル図から検証用コードを自動で生成できるため、設計者がモデルから自力でコーディングをする必要がありません。
不具合に至る遷移を自動で抽出し、結果をアニメーション動画で確認できるため、モデルや仕様の不具合が直感的にわかり、検証作業の効率をさらに高めることができます。
EAとDynaSpecを導入することで、不具合を早期に発見し、設計品質を向上させることが可能です。
従来の方式の問題点
-
自然言語による曖昧な表現で仕様理解に齟齬が発生
-
システム設計において、仕様を自然言語で表現すると、あいまいな箇所が残ったり、理解の齟齬が発生します。
-
理解の齟齬を減らすためには、自然言語ではなくUML/SysMLなどの図表表現を使用することが有効です。
-
-
熟練者への依存
-
これまでの上流設計の検証は、基本的に熟練者のレビューにより行われており、熟練者が退職や異動してしまうとレビューの質を担保できなくなってしまいます。
-
UML/SysMLによる設計でも設計者の習熟度が充分でないと、設計者自身が設計の正確性と妥当性を確認することができないため、レビューは熟練者に依存せざるを得ません
-
-
不具合の見逃し
-
熟練者によるレビューが充分に行われないと、設計に矛盾や漏れが含まれたまま下流の工程に進んでしまいます。
-
また、仕様の複雑化により、熟練レビュアーですら見逃してしまう不具合は実際に存在します。現行の熟練者レビューは、熟練者が経験に基づき設計に含まれそうなシナリオを考え、頭の中でシミュレーションを行うような形で行われますが、いくら熟練者であっても人間の力には限界があり、抜け漏れをゼロにはできません。
-
Dynaspecによる3つの軽減
-
理解の齟齬を軽減
-
自然言語ではなくUML/SysMLモデルを用いて設計を行うことで曖昧な表現をなくします。
-
UML/SysMLという共通のUI・言語を使用することにより、複数人の作業でも、仕様への理解の齟齬が軽減します
-
-
熟練者への依存を軽減
-
設計が正しく行われているか、設計者自身で検証できるので、熟練者への依存が軽減します。
-
-
熟練者の負荷を軽減し、不具合の見逃しを軽減
-
これまでの上流設計の検証は、熟練者が経験に基づいて頭の中でシミュレーションを行い、発生しうる不具合とその発生箇所を特定することで行われてきましたが、DynaSpecがあれば、シミュレーションのステップをコンピューターに任せることができます。熟練者は、コンピュータの提示する結果をもとに、設計が仕様通り・想定した通りになっているかの判定に注力することができます。
-
なぜモデル検査が有効なのか
これまでの上流設計の検証は、基本的に熟練者のレビューにより行われてきました。しかし、熟練者が退職してしまったり、または熟練者すらも想像がつかないような難しい設計を強いられる場面も増えてきているのではないでしょうか。
モデル検査は、形式検証における1手法であり、動的なモデルを網羅的に検査することによって、ヒューマンレビューやシミュレーションでは発見が難しい不具合を発見できる手法です。
「ソフトウェアバグの原因の8割は上流設計の不具合」とも言われる中で、「上流設計から網羅的な検査を行うこと」の意義は日増しに高くなっています。
DynaSpec は専用言語の習得など導入ハードルが高いモデル検査を気軽に実務で利用できるよう開発されました。
ツールの導入から運用まで一貫したサービス
-
DynaspecはEAのアドインツールです。既にEAをお使いの環境であれば、導入は簡単。
-
EAをお使いでない場合は、EAの導入からお手伝いいたします。
-
ご希望に応じて、運用に至るまで、手厚くサポートを行います。
-
DynaSpecトレーニング
-
コンサルティング
-
UML/SysMLモデリングのレクチャー
-
お客様の実際の題材を用いたモデル化支援
-
-