第8回クリティカルソフトウェアワークショップ（WOCS2011）において、ソフトウェア基盤技術課、米田、中本が「中小企業の形式手法への取り組み」と題して講演を行いました。

【第8回クリティカルソフトウェアワークショップ】

2011年1月18日、19日に開催された第8回クリティカルソフトウェアワークショップの信頼性関連セッションにて、形式手法の取り組みへの研究成果についてお話させていただきました。

サニー技研は、経済産業省中小企業庁の戦略的基盤技術高度化支援事業に採択された「機能安全対応自動車制御用プラットフォームの開発」におけるCAN/FlexRay通信ミドルウェアの機能安全活動や、産官学の研究プロジェクトである組込みシステム形式手法研究会に参画し、機能安全や形式手法の研究活動にこれまで取り組んできました。

これらの研究活動の中では、サニー技研から実際の開発において想定される事象に近い例題を提示し、様々な形式手法を実践して研究しています。

このたびは、中小企業の実務者の視点で、形式手法導入における知見や有用性、各形式手法の比較などをご紹介させていただきました。

研究活動の中で実践した実例を挙げながら様々な形式手法を解説し、少しの学習で活用できる点や、各形式手法の導入試用による比較、形式検証を行うべき適用範囲の知見など、実務者レベルでの活用をご紹介させていただいたところ、各方面から大変ご好評をいただくことができました。

導入のハードルが高いと思われている形式手法を、このたびの講演で導入の一助になれば幸いです。

サニー技研は、今後も組込みシステム形式手法研究会の活動を通して形式手法の実践研究と普及に努め、日本の安全技術の発展に貢献してまいります。

■クリティカルソフトウェアワークショップ概要

急速な技術革新に伴い、システムの大規模化及び複雑化が進む現在、ソフトウェアが更に重要な役割を担っています。宇宙、航空、原子力、鉄道、自動車などのクリティカルシステムにおいてはソフトウェア開発・保守・運用に関する技術の向上が安全で信頼性の高いシステムを構築する上での重要な鍵となります。
本ワークショップでは、クリティカルソフトウェアに焦点を当て、これに携わる技術者・研究者の情報交換の場を提供し、特に産業分野の枠を越えた交流を図ることにより日本におけるクリティカルソフトウェアに関する技術向上の一助とすることを目的として開催します。
（公式サイトから：http://stage.tksc.jaxa.jp/jedi/event/20110118.html）

■形式手法とは

数学的理論を背景にしたソフトウェアおよびハードウェアの仕様記述、開発、検証の手法を形式手法（Formal Method）と呼ばれます。
形式手法を用いて仕様記述を洗い出すことで、仕様不備や曖昧さ、矛盾を排除して開発工程でエラーが入りこまないことを保証します。高度な信頼性・安全性が求められるシステムにおいては、その利用が特に重要とされています。

■組込みシステム形式手法研究会

財団法人 名古屋産業科学研究所の産官学連携による研究会です。
「リアルタイムOSなどの組込みソフトウェアおよび組込みシステムを対象として形式仕様記述及び形式検証技術によるシステム設計及び検証の実例を積み上げ、産業応用上の知見を蓄積し、その知見を公開することにより、産業界の技術向上に資することを目的とする。」

（研究会設立趣意書から抜粋：http://www.nisri.jp/dor/groups/2009_4.html）