ゼミナールI講演

日時: 平成26年5月19日(月)3限 (13:30 -- 15:00)
Mon., May 19th, 2014 (3rd Period, 13:30 -- 15:00)
場所: L1

講演者: Cyrille Artho (セキュアソフトウェアシステム(連携)・独立行政法人 産業技術総合研究所)
(Secure Software Systems (Collaborative Lab)/National Institute of Advanced Industrial Science and Technology)
題目: Software Reliability and Test-based Software Verification
ソフトウェア信頼性とテスト指向のソフトウェア検証
概要: In these days, reliability of software, especially in embedded applications, is critical. Buggy behavior of embedded software may harm or even kill its users, and such fatalities are indeed reported in the real world.

We will introduce how software reliability can be treated, studied, and assured in the real software development processes. In the first part, we will introduce several techniques which can be applied for various kinds of software, including software verification, model checking, and language-based approaches. Modern tools can test many kinds of properties that cannot be directly observed through the output of software, but still show underlying defects, ranging from memory corruption to subtle concurrency problems.

In the second part, we will focus more on the most practical technique on the field, software testing. Even though testing cannot fully verify software, it is scalable and effective thanks to a continuous increase in test automation techniques. We will present how test frameworks have evolved and are moving towards model-based approaches that increase automation even further.

近年特に組込み分野において、ソフトウェアの信頼性は非常に重要な問題になっている。組込みソフトウェアの誤動作は時にユーザのけがや命にも直結することがあり、残念なことにそのような事例が実際に報告されている。

今回の講演では、ソフトウェア信頼性の考え方、研究、そして実際のソフトウェア開発プロセスでの取扱い方について紹介する。最初に、問題の概観を説明するとともに、近年はメモリ破壊や並列動作の問題など、プログラムの出力には直ちに現れないような欠陥を調べるような技法が多く開発されており、ソフトウェア検証、モデル検査、プログラミング言語処理系による対策など、いくつかの対策技法についてその概要を紹介する。

後半では、現在実際の開発で最も広く使われている「ソフトウェアテスト」について深掘りする。テストはもちろん全ての誤りを見つけられるわけではないが、大規模なソフトウェアへも非常に良く適合し、自動化技術の進歩とともに実効性も向上し続けている。テスト基盤のこれまでの発展や、今後の重要な方向性の1つである「モデルベースの技法」について深く説明する。

ゼミナール I, II ページへ