セーフティクリティカルソフトウェア向けのエンジニアリングソリューション。
構想から実装、運用まで、ソリューションをお客様のアーキテクチャ、ツールチェーン、プロセス環境に組み込みます。
後付けではなく、アーキテクチャに組み込むソリューション。
ソフトウェアデファインドシステムへの移行により、リリースサイクル、バリアント空間、デプロイモデルは変化します。一方で、機能安全とエビデンスに対する要求の厳格さは変わりません。
BTC Embedded Systems のソリューションは、お客様のチームだけで統合する既製ツールではありません。形式検証を基盤として、お客様のアーキテクチャ、ツールチェーン、プロセス環境に組み込みます。
検証は単なる機能ではありません。すべてを支える基盤です。
セーフティクリティカルな用途に向け、BTC Embedded Systems は形式手法で担保された決定論的コアを基盤とします。私たちの原点は、形式検証と大学研究です。モデル検査、定理証明、制約求解、自動テスト生成は、25 年にわたり中核的な専門領域であり続けています。お客様のチームには、日々のエンジニアリング業務で使いやすく、統合しやすいソリューションを提供します。その背後にある数学的な複雑さは、私たちが引き受けます。
BTC QCore
製品、顧客固有ツール、コンサルティング提供を支える基盤。
効率的なソリューション開発には、ソフトウェア品質の基盤である BTC QCore を活用します。QCore は、実績ある主要技術を、構成可能な一つの技術基盤に集約しています。残るギャップは的を絞ったカスタム開発で補います。汎用ツールキットに伴う妥協を避けながら、再現可能な品質で新たなソリューションを迅速に構築できます。
取り組みの出発点は、新規ソリューション、既存のシステム環境、技術的負債を抱えたコードベース、自動化の機会など、それぞれ異なります。流行ではなく、エンジニアリング上の判断に基づいて手法を選択します。
構造的なエンジニアリング課題を解決した事例。
各事例では、セーフティクリティカルな開発における具体的なボトルネックを起点に、再現可能なエンジニアリングワークフローへ変換しています。
バリアント空間の全数テストは不可能でも、テスト対象の選択には説明可能な根拠が必要です。
構成自由度の高い製品ラインでは、全数テストが現実的でないほど巨大な構成空間が生まれます。経験則による選択は拡張できず、監査にも耐えません。見落とされた機能間の相互作用は市場で初めて顕在化し、リコール費用と評判に実害をもたらします。
QCore 技術基盤の制約ベース手法を用いて、構成空間全体に対する数学的根拠のあるカバレッジ保証とともに、実際にテストが必要な最小限のバリアント集合を特定します。管理不能な組み合わせ問題を、証明可能で監査対応のテスト戦略へ変換します。
バリアント管理が手作業で制御できる限界に達し、既製ソリューションでは要求を満たせず、選択したテストが本当に十分であることを証明する必要がある場合。
理論上およそ 10²⁵ 通りのバリアントを持つメーカーに対し、テスト対象を形式手法で保証された運用可能な規模へ絞り込みました。証明可能で、再現性があり、監査にも対応できます。
10²⁵ 通りのバリアント。どれをテストし、それで十分だとどう証明するのか。
バリアント空間の全数テストは不可能でも、テスト対象の選択には説明可能な根拠が必要です。
構成自由度の高い製品ラインでは、全数テストが現実的でないほど巨大な構成空間が生まれます。経験則による選択は拡張できず、監査にも耐えません。見落とされた機能間の相互作用は市場で初めて顕在化し、リコール費用と評判に実害をもたらします。
QCore 技術基盤の制約ベース手法を用いて、構成空間全体に対する数学的根拠のあるカバレッジ保証とともに、実際にテストが必要な最小限のバリアント集合を特定します。管理不能な組み合わせ問題を、証明可能で監査対応のテスト戦略へ変換します。
バリアント管理が手作業で制御できる限界に達し、既製ソリューションでは要求を満たせず、選択したテストが本当に十分であることを証明する必要がある場合。
理論上およそ 10²⁵ 通りのバリアントを持つメーカーに対し、テスト対象を形式手法で保証された運用可能な規模へ絞り込みました。証明可能で、再現性があり、監査にも対応できます。
エンジニアリングチームにご相談ください。
エンジニアリング上の課題がどこにあるかをお聞かせください。ソリューションで解くべきか、コンサルティングが必要か、あるいはその両方かを見極めます。