曖昧さ → 誤ったシステム
形式化されていない要求は、エンジニアによって解釈が異なります。「速い」「直後」「安定」などの曖昧さを読み手がそれぞれの解釈で補うため、誤読した要求を正しく実装しても、できあがるのは誤ったシステムです。
自然言語の要求
イネーブル信号の後、ブレーキコマンドは安定しなければなりません。安定までの期限は短時間以内です。
形式化済み（Universal Pattern）
トリガーenable == true
アクション|brake − target| ≤ 0.5
以内t ≤ 20 ms
すべての入力とキャリブレーションで証明済み
モデル検査 · 到達可能な違反なし
課題
自然言語には解釈の余地が残ります。
記述された要求と安全なシステムの間には 2 つのギャップがあります。テストをいくら実行しても、どちらも埋まりません。
テスト → 未解決の問い
テストで確認できるのは、試すことを想定した挙動です。すべての入力、状態、キャリブレーションを網羅することはできないため、「安全要求が違反される可能性はあるか」という本質的な問いは、テストスイートがすべて合格した後も残ります。
テストはサンプリングです。 形式検証は証明です。
形式手法は両方のギャップを埋めます。要求を厳密に定義し、コードがその要求を満たすことを証明します。
形式仕様
直感的な言語。
BTC Universal Pattern は、要求エンジニアリングのための直感的なグラフィカル手法です。エディターとドキュメントが同一の成果物となります。満たすべき条件を記述すると、ツールが機械可読な形式へ変換し、元の要求へのトレーサビリティを一貫して維持します。
要求を機械可読にする 3 つのステップ
1特定
該当表現をマーク
要求内の意味のあるフレーズを強調表示し、再利用可能なマクロに変換します。
［有効化］の後、
［ブレーキが安定する］
2構造化
構造とタイミングを定義
マクロをトリガー、アクション、タイミングとしてグラフィカルに配置します。このパターンによって曖昧さが解消されます。
トリガー：有効化
アクション：ブレーキが安定
20 ms 以内
3対応付け
インターフェースに対応付け
各マクロを実際のシステム信号に対応付けます。これにより、要求は機械可読かつ実行可能になります。
enable → ctrl.en
brake → act.trq
✓ 機械可読
元の要求への双方向トレーサビリティを、すべてのステップで維持します。
信頼性の高い AI
AI 支援による形式化、その欠けていた要素。
形式仕様を人手で記述することは困難でした。要求の形式化は本質的に言語を扱う作業であり、まさに現在の AI が得意とする領域です。
BTC AI Assistant は、記述された要求からトリガー、アクション、タイミングを含む Universal Pattern の草案を作成します。内容を調整・承認したり、そこからテストケースを生成したりできます。
形式検証
検証プロセスに役立つ3つのユースケース。
機械可読な要求＝自動検証。
01
フォーマルテスト
既存のすべてのテストケースを、形式化したすべての要求と一括で照合します。追加のテスト工数をかけずに、元のテストでは確認対象としていなかった副作用も検出します。
02
自動テスト生成
モデル検査は、テストスイートに不足しているテストケースを正確に生成し、試行錯誤ではなく決定論的に要求カバレッジを 100% まで高めます。
03
形式検証
モデル検査は、要求に違反し得ないこと、すなわち入力とキャリブレーションのどの組み合わせも危険な状態に到達しないことを数学的に証明するか、具体的な反例を返します。
主な利点
形式手法から得られるもの。
より良い要求
形式化によって記述の精度が求められるため、曖昧な要求をコードやテストの作成前に検出できます。
意味のあるカバレッジ
要求カバレッジは推定ではなく自動的に測定され、不足も自動的に解消されます。
副作用の検出
すべてのテストをすべての要求と照合し、追加工数なしでリグレッションを明らかにします。
100% カバレッジ
自動生成されたベクトルで不足を補い、完全な要求カバレッジを達成します。
100% の証明
すべての入力とキャリブレーションにわたる保証。
自社コードで証明。
評価ライセンスには、実際の要求の 1 つを対象にエンドツーエンドでセットアップする、当社エンジニアとの導入ワークショップが含まれます。