本日は、6月30日弊社開催のWebinarにて形式手法の活用の事例をご紹介頂いた株式会社ジェイテクト ステアリングシステム統括部上席主担当　米木真哉様に自社の製品開発へ形式検証を使用するに至る経緯や、これまでの自社の取組でのSPARK適用の効果や課題などのお話を伺いました。

先日はWebinarでのご講演ありがとうございます。本日は御社の開発において、形式検証を適用することになった経緯や、AdaCore社のSPARKにこれまで取り組んできて良かった点や課題となる点について、お話を伺えればと思います。よろしくお願いいたします。

●はじめに、御社の事業紹介をお願いします。

「弊社の柱となる事業として、電動パワーステアリング（EPS）があります。1988年に量産、生産開始から現在まで世界トップシェアを維持しており、より安全で快適な、自動運転に対応する技術研究開発をすすめています。」

●形式検証を使用するに至る経緯は何ですか？

「自動運転やステアバイワイヤ等の技術開発の過程で、ソフトウェアの安全性の論証が課題となったことが直接の背景になります。自動運転やステアバイワイヤでは、ソフトウェアの不具合が安全上重大な影響を引き起こす可能性があることから、従来のソフトウェア開発に加えて、形式検証を用いることで本質的にソフトウェアの不具合を開発の早い段階で確実に排除できる可能性があると考えました。」

●SPARKに決定した理由を教えてください。

「SPARKは自動車業界以外では既に実績を積み上げていること、開発環境が比較的しっかりと整備されていること、の2点が大きな理由になります。」

●SPARKをどのようなプログラムに応用していますか？」

「現時点では、どのプログラムから適用すべきかについて、実際の製品ソフトを例題に検討を進めているところですが、先ずは小・中規模のソフトウェアコンポーネントから徐々に適用範囲を拡げていくことを検討しています。」

●SPARKのプログラムの適用範囲、方法を教えてください。●

「上記3.のとおり、現時点では明確に適用範囲を決定した訳ではありません。C言語との共存させることも可能であることから、SPARKの持つ機能とC言語に対する既存の検証の枠組みとを有機的に融合させ、より高いレベルで安全性の論証が提供できるようにするという利用方法を検討中です。」

●Contractの適用は、容易に行えましたか？

「論証したい内容にもよりますが、特に定理証明を行う際のcontractについては、ある程度以上のノウハウが必要と感じています。」

●御社からみたSPARKの長所、短所を教えてください。

「現状分かっている長所としては、コーディングの時点で検証をほぼ平行して行えること、結果として単体テスト項目ができる可能性があることがあります。将来的には演算処理結果が安全上許容可能な範囲を逸脱しないことの検証といった、テストだけでは完全に論証することが難しい領域への応用についても、潜在的な長所と捉えています。また、これらの様々な観点からのソフトウェアの静的な検証を全て一つのツールで行うことができることも利点であると考えます。

一方、短所ですが、プログラムをAda/SPARKで作成する必要があることが挙げられます。現在、組込みソフトウェアエンジニアの大半がC言語に慣れていることもあり、新たにAda/SPARKに取り組まなくてはなりません。また同じ理由から、C言語で記述された過去のソフトウェア資産が利用できなくなることも短所のひとつと考えます。」

●SPARKの拡張性（モデルベースへ）は考えていますか？

「モデル開発への適用について、現時点では具体的な計画はありません。しかし、モデルで記述した制御仕様の検証にSPARKが応用できるのであれば、取り組んでみたい題材であると考えます。」

「まずは、弊社のソフトウェア開発の中で、複雑なcontractを記載せずに、比較的容易にSPARKの特徴が生かせるユースケースを洗い出すことが当面の目標になります。その上で、実際の製品開発の中で、段階的にそれらのユースケースに対してSPARKの導入を進めて行くことまでが最初のステップになります。

次の段階として、contractを積極的に活用しソフトウェアの演算結果に対する安全性の論証に駒を進めて行きたいと考えています。」

ジェイテクト 米木様

米木様、どうもありがとうございました。Webinarおよび本対談で御社が形式手法に取り組んでいる経緯やこれから直面されるであろう課題など、いろいろとお話を頂戴できまして大変参考になりました。また今回挙げられた課題を越えた際には、またお話をお聞かせください。

公開日：2021年11月15 日