ソフトウェアシステムのリスク低減に対する形式手法からのアプローチ - NII SEEDs / 国立情報学研究所

研究シーズ2014ソフトウェア科学

# ソフトウェアシステムのリスク低減に対する形式手法からのアプローチ

中島 震アーキテクチャ科学研究系　教授

研究分野形式手法／耐リスク／ソシオテクノ

## 研究背景・目的

ソフトウェアシステムが社会基盤の重要な構成要素となる時代が到来しました。装置機器を中心に発展してきた産業分野や応用セクターが次々とソフトウェア化しています。つまり、ソフトウェア抜きに、イノベーションを考えることができません。新たなサービスの実現にソフトウェア技術が中心的な役割を果たすからです。ソフトウェアシステムは私たちの日常生活を支えることから、求められる信頼性を達成する技術への関心が高まっています。一方、「当たり前の不具合」という言葉に代表されるように、ソフトウェアに絶対的な信頼性はあり得ません。期待される安全性を明確化し、ソフトウェアシステムがもたらすリスクの低減をすることが求められます。本研究課題は、形式手法や自動検証の方法を用いて、このリスク低減問題に科学的な方法を導入することを目的としています。

### 研究内容

20世紀のソフトウェア工学は生産性向上の技術確立が主要な課題でした。ところが、多くの失敗プロジェクト経験を経て、品質の高さが生産性の向上につながることが認識されています。そこで、高い信頼性を目指す技術開発に重心が移り、形式手法や自動検証の方法を活用したソフトウェア開発が関心を集めるようになりました。テクノサイエンスによる方法であり、適用限界の範囲で活用法を示します。本研究課題は、産業界との協業経験を踏まえて、理論と実践の両面から「うまく使う方法」を集積する一方、従来のソフトウェア工学手法と自動検証の組み合わせによるプログラム信頼性向上を実現します。また、ソフトウェア開発で重要な技術移管が教育の問題を含むものであると考え、形式手法の基礎を学習するカリキュラムを整備しました。しかし、ソフトウェアシステムがもたらすリスク低減を考える際、大規模システムの挙動を正確に把握できないという本質的な問題に遭遇します。定量的な機能外要求を対象として、現状の還元論による方法に加えてシステム思考を採り入れたソシオテクノサイエンスの研究を行っています。

### 産業応用の可能性

形式手法および自動検証の基本を学習する標準カリキュラム
不具合のあるプログラムの欠陥箇所を自動発見することでテスト工程の工数を削減
モデルベース解析によって開発上流工程で定量的な機能外要求の妥当性を確認

##### 連絡先

中島 震［アーキテクチャ科学研究系　教授］
http://researchmap.jp/nkjm/

## Recommend

### 機械学習ソフトウェアの品質向上

ソフトウェア科学

中島 震

情報社会相関研究系 教授

### 機械学習の過程や結果を見える化し
安全性分析や開発プロセスに生かす

ソフトウェア科学

吉岡 信和

アーキテクチャ科学研究系 准教授

### 「形式手法」をものづくりへ
高品質・高効率な製品開発に向けて

ソフトウェア科学

蓮尾 一郎

アーキテクチャ科学研究系 准教授／システム設計数理国際研究センター長

### ソフトウェアの挙動を検証
安全性と生産性の両立めざす

ソフトウェア科学

関山 太朗

アーキテクチャ科学研究系 助教

### 実世界と機械学習の不確かさに挑む
ソフトウェアの品質向上と保証

ソフトウェア科学

石川 冬樹

アーキテクチャ科学研究系 准教授

### 屋内もスマホでナビゲーション音響測位、可視光通信技術

橋爪 宏達