国際規格にて、セーフティ・クリティカルなソフトウェア開発に形式手法が必要とされております。
弊社では、実開発プロセスへの形式手法（Event-B、Bメソッド）導入を、組込みソフトウェア向け開発プロセスガイド（ESPR）に従って研究を進めており、各プロセスへの形式手法導入方法、開発ドキュメントとの整合技術を提供できます。

ツールイメージ

Event-B
（上流工程向けに特化した手法）

RODIN platform ProB Animator
http://www.event-b.org/
 
 

ツールイメージ

Bメソッド
 

Atelier-B
http://www.clearsy.com/
■　証明項目の自動生成機能
■　自動証明　　 ※容易な技術習得・効率化