​特徴・機能

形式検証の導入メリット

​

​これまでの上流設計の検証は、基本的に熟練者のレビューにより行われていたと思います。

​

しかし、熟練者が退職してしまったり、または熟練者すらも想像がつかないような難しい設計を強いられる場面も増えてきているのではないでしょうか。

​

「ソフトウェアバグの原因の8割は上流設計の不具合」と言われることもある中で、「上流設計から網羅的な検査を行うこと」の意義は日増しに高くなっています。

​

「形式検証・モデル検査」は、シミュレーションよりも強力に、設計モデルを検証することのできる技術です。

形式検証・

モデル検査とは？

形式検証とは、複雑なソフトウェアの開発において、設計段階から不具合を発見することを可能にする手法です。

​

モデル検査とは、形式検証における1手法であり、動的なモデルを網羅検査することによって、ヒューマンレビューや、シミュレーションでは発見することのできない不具合を抽出することのできる手法です。

​以前は導入ハードルが高いと思われていたモデル検査ですが、モデル化の工夫や、AWSなどの仮想環境を併用することで、十分実務に適用することが可能です。​
 

Enterprise Architect上で作業を完結することが可能

DynaSpecはSparx Systems Japan社が販売するEnterprise Architect(以下EA)のアドインツールです。

DynaSpecを用いることで、EA上で作成したUMLモデル内の不具合を自動で抽出することが可能です。

​

また、DynaSpecの可視化機能では、抽出した不具合に至る遷移ログを、EA上でアニメーションで確認することができ、検証作業の効率を更に高めることができます。

​

EAとDynaSpecを導入することで、ダイアグラムにより分かり易く仕様を表現し、作成したモデルを動かして検証することができ、動く仕様(Dynamic Specfication)で設計品質を向上させることができます。

​ツールの導入から運用まで一貫したサービス

​

KKEの形式検証ソリューションはツールの売り切りではありません。

​

ツールの使用方法と共に、UMLのモデル化方法に関するレクチャー、或いはお客様の実際の題材を用いたモデル化支援等も行い、運用に至るまで、手厚くサポートを行います。

事例

​​JAXA

宇宙航空研究開発機構(国研) 様

SED

宇宙技術開発(株) 様

​

「自律飛行安全システムの開発」に​形式検証を適用した事例

JR 東日本

東日本旅客鉄道株式会社 様

​

「駅構内踏切の警報／遮断制御」に​形式検証を適用した事例

​自動車 OEM

某自動車OEM 様

​

「HVの走行モード切替制御」

に​形式検証を適用した事例

上記事例にご興味のある方は下記から紹介資料を無料ダウンロードしてください

まずはお気軽にご相談ください

​

現在、お問い合わせはメールにて承っております。​

​

構造計画研究所

DynaSpecチーム

03-5342-1066　

aor-bizdev@kke.co.jp 

​

個人情報保護方針　会社情報