メソドロジがすべて
最も優れた最もシャープな鉛筆を使っても、すべてのものが思い通りに描けるわけではありません。ツールを最大限に活用するには、描きたいものの寸法や割合など必要条件を明確に理解することが不可欠です。
フォーマル検証では、それが必須です。フォーマル検証の導入を成功させるメソドロジについての十分な理解が必須であるにも関わらず、ほとんどのフォーマル検証トレーニングのプログラムにはそれが欠けているのです。ほとんどのプログラムは、一方では使用するアサーション言語やその最新の構文的拡張に、他方ではEDAツールキットとその機能にあまりにも注力し過ぎています。
フォーマル検証のパラドックス
フォーマル検証トレーニングに見られるこのような現状と、優れたメソドロジへの注力が欠如しているために、エンドユーザーは極端なフォーマル検証の使い方をすることになり、完全に不健全なフォーマル検証のパラドックスが生じます。すなわち深い理解、つまりエンドツーエンドの検証に取組むフォーマル検証の第一人者がいる一方で、他方ではフォーマルアプリのみを使用するエンジニアチームが、ツールの完全自動化された側面のみを使っています。
残念ながら、このようなユースモデルのどちらもが、コーナーケースのバグを特定したり、頻繁に必要となる設計の特性を網羅的に証明したりする上で、その可能性をフルに引出せるような包括的な展開には至っていません。このスペクトラムの中間には、アサーションを利用するエンジニアのチームも存在します。しかしこのほとんどは組織化されておらず、体系的には展開されていません。アサーションは非常に単純な振舞いをチェックする単純なポイントベースのアサーションに限定されていることが多く、ここでもフォーマル検証の潜在能力を十分に引き出せてはいません。
Axiomiseでは、フォーマル検証によって機能検証の主な課題を解決する上で必要な、上記のギャップを経験することに注力しています。私たちはフォーマル検証が大規模設計に適応できるようなメソドロジを専門としています。
スケーラブルなフォーマル検証は、博士号が必要となるような伝説的な話ではなく、優れたトレーニング、コンサルティング、サービスを組合せたモデルによって適切に学び、適用することができます。私たちがこの分野で正視してきたことは、エンジニアがフォーマル検証メソドロジの基本的かつ高度なスキルを充分なトレーニングによって身につければ、プロジェクトに着手することは可能ですが、多くの場合、検証プランや戦略、詳細な実行に関するフォローアップ指導、サポート、支援が必要だということです。Axiomiseはトレーニング、コンサルティング、サービスの組合せにより、フォーマル検証を可能にする多方面からのアプローチを提供します。
Consulting
Axiomiseではコンサルティングの機会にお客様のビジネスにおけるフォーマル検証の位置付けを確認し、お客様のニーズを把握し、そしてお客様のニーズに合ったアドバイスをさせていただきます。Axiomiseはお客様のビジネスを第一に考え、お客様のフォーマル活用の課題をサポートしたいと考えています。私たちはエンジニアにフォーマルのスキルとメソドロジをトレーニングすることは最初のステップとして有効ですが、フォーマルを最大限に活用するためには、トレーニングの前後に継続的なサポートとアドバイスが必要であることを理解しています。
詳しくはコンサルティングプロミスをご覧ください
Services
場合によっては、フォーマル検証のトレーニングを受けて実践する第一歩を踏み出す人員を、組織が有していないこともあります。このような場合、Axiomiseはターンキー・プロジェクトの実行を請け負う、独自のサービスの可能性を提供します。詳細については、info@axiomise.com までお問い合わせください。