北陸先端科学技術大学院大学情報科学研究科青木研究室
Japan Advanced Institute of Science and Technology, School of Information Science, Aoki Lab
ブース番号
UI-002
石川県能美市旭台1-1
[TEL] 0761-51-1906[URL] http://www.jaist.ac.jp/
Asahidai 1-1,Nomi,Ishikawa,JAPAN
[TEL] 0761-51-1906 [URL] http://www.jaist.ac.jp/
出展の見どころ
現在,形式手法・形式検証手法が関心を集めており,安全性や信頼性に関する国際規格にも採り入れられるようになってきた.本研究室では,このような形式手法・形式検証手法を実開発に応用する手法について研究を行っている.本展示では,形式検証手法の1つであるモデル検査に焦点を当て,以下の研究成果について紹介する.

1)RTOSの検証と支援ツール.RTOS(Real-Time operating System)はソフトウェア実行の共通基盤であるため,それ自身にも高い信頼性が求められる.我々は,これまでに,モデル検査ツールを用いてRTOSの設計検証を行う手法,および,支援ツールを開発してきた.そこで,本展示では,開発した支援ツールとOSEK/VDX RTOSを対象とした検証例について紹介する.

2)マルチタスクソフトウェアの設計検証支援ツール.RTOS上で動作するマルチタスクソフトウェアでは,並行動作に起因する様々な問題が生じるが,それらは,再現
性が低いため発見が難しい.モデル検査は,このような問題の検出を得意としている.我々は,モデル検査を実適用するための仕組みや支援ツールを開発しており,
本展示では,それらの研究成果について紹介する.



【close】