安全性の証明

近年、製品ユーザー、また、社会から、製品の安全性の説明が求められています。アトリエでは、国際規格でも推奨されている「形式手法」技術を利用して安全性の証明を支援します。

形式手法は、数学および論理学に基づくシステムモデリングおよびプロパティ検証の技術です。設計に矛盾がないことを論理的に証明することで、堅牢かつ再利用性の高いアーキテクチャとバグのないコードを実現します。海外の鉄道システムを中心に、高いレベルの安全性および信頼性が求められるシステムで実用化されている手法であり、産業界での実用レベルに達している手法です。
しかしながら、わが国では導入が進んでいないのも事実です。 その理由として、ツールをインストールしたり、教科書を読んだりしても、 実際の開発に対してどのように使用すればよいか理解が難しいことがあります。

アトリエでは、ソフトウェア開発のためのBメソッドによる形式モデリングに経験と知見を有しており、 効率的な導入を支援します。

課題の定義と論証

形式手法の適用にあたってまず大事なことは、証明したい性質を明確にすることです。その上で、性質を論理式として記述する必要があります。その際には、証明したい性質を網羅的かつ正確に、論理式に翻訳する必要があります。
アトリエでは、論理式のパターン化により、効率的な作成を支援します。またそれに先立って、そもそも証明すべき事柄は何であるのかを明確にするために、要件分析に立ち返った支援を行います。

モデリング

定義した課題を解くにあたり、ツール(計算機)が理解可能な形式に表現するのがモデリングです。アトリエでは、数ある形式手法の中でも特にシステムモデリングを得意とするEvent-Bや、ソフトウェア開発全般をカバーするBメソッドによる形式モデリングの知見と経験を有しており、効率的な導入を支援します。また、SPINやProBによるモデル検査技術の導入も支援します。

網羅的な検証/証明

形式手法による検証には、対話型証明によるものとモデル検査によるものがあります。いずれもツールによる自動証明を行いますが、問題のサイズによっては、結果が得られない可能性があります。アトリエでは、対話型証明の自動証明率を向上させるためのモデリング、モデル検査の状態爆発を回避するためのモデリングに知見を有しており、効率的な検証を支援します。