​どんなにテストをしても抽出できない不具合はありませんか？

どんなにシミュレーションを重ねても検出できない不具合はありませんか？

MBEC(Model Based Error Checker)は、形式検証・モデル検査と呼ばれる

手法を用いて、システムレベルでの設計検証を強力にサポートします。

シミュレーションでは抽出できない不具合も

MBECなら抽出することが出来ます

​TOPICS 

2020年3月13日(金) フロントローディングによる設計品質向上セミナーを開催します。

​どんなにテストをしても抽出できない不具合はありませんか？

どんなにシミュレーションを重ねても検出できない不具合はありませんか？

DynaSpec(Dynamic Specification)は、形式検証・モデル検査と呼ばれる

手法を用いて、システムレベルでの設計検証を強力にサポートします。

シミュレーションでは抽出できない不具合も

DynaSpecなら抽出することが出来ます

​TOPICS 

6月26日(金)に開催いたしました「フロントローディングによる設計品質向上Webセミナー」
の開催レポート、Q&AをBlogに公開しました。

モデルベース形式検証ツール「MBEC」は新たに「DynaSpec」として2020年4月より正式に販売を開始しました。現在、Web会議によるプレゼン、デモの実施や、ツール試用、試解析、資料DL等、各種ご相談を承っておりますのでお手軽にお問合せ下さい。

新型コロナウィルス対策として現在弊社では可能な限りテレワークを実施しております。

資料ダウンロード以外のお問合せにつきましても、下記リンク先のお問合せページにて、お問合せを頂ければ幸いです。

​特徴・機能

形式検証の導入メリット

​

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

​

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

​

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

​

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

形式検証・

モデル検査とは？

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

​

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

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

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

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

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

​

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

​

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

事例

​​JAXA

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

SED

宇宙技術開発(株) 様

​

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

JR 東日本

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

​

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

​自動車 OEM

某自動車OEM 様

​

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

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

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

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

​

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

​

構造計画研究所 事業開発部AOR研究室

03-5342-1065　

 

​

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