開催日時： 平成17年10月7日（金） 9:30-17:00
*10/17から変更になりました
開催会場： 東京電機大学
神田キャンパス７号館1F 丹羽ホール（東京都千代田区神田錦町2-2）
コーディネータ：岸 知二（北陸先端科学技術大学院大学）
【セミナー概要】
形式的手法はやたら難しく、また小さな問題にしか適用できない研究室の技術だと考えておられる方も多いと思いますが、すでにさまざまな事例に適用されている実用的な技術です。本セミナーでは、組込みソフトウェア開発への適用という側面に焦点をあて、その技術をコンパクトかつ分りやすく紹介します。
【プログラム】
セッション１ 9:30-10:30 「組込みソフトウェア開発と科学的手法」
片山 卓也（北陸先端大）
【講演概要】組込みソフトウェアはそのサイズが余り大きくなかったこと，また，資源制約が強かったことなどもあって，その開発には最新のソフトウェアテクノロジーが用いられてこなかった．しかし，高度なユーザーインタフェースや通信機能など製品に要求される機能が高級化し，組み込まれるソフトウェアが大規模化・複雑化したことにより，これまでのソフトウェア開発方法論が十分に機能しなくなりつつある．最新のソフトウェア開発技術を組込みソフトウェアの開発への投入，あるいはそのための技術開発を行うことが強く求められている．本講演では，形式検証，オブジェクト技術，プロダクトライン開発，ＭＤＡなど，今後の組込みソフトウェアの開発に必要となるソフトウェア技術について概説する．
セッション２ 10:40-12:20 「検証技術-モデル検査と定理証明」
青木 利晃（北陸先端大）
【講演概要】ソフトウェア検証のための技術としては，大きく分類して，モデル検査技術と定理証明技術がある．モデル検査技術では，有限状態モデルを網羅的に探索して，デッドロックや飢餓状態などの望ましく無い状況を自動的に検出できる．しかしながら，無限の状態を持つものや，有限でも多くの状態を持つものは取り扱うことができない．一方，定理証明技術では，定理や推論規則を用いて証明を行うため，そのような状態を持つものでも取り扱うことができるが，対話的な推論が必要になる．このように，これらの技術には，それぞれに長所と短所があり，検証する性質により使い分けが必要である．本講演では，それぞれの技術の概要と特徴について，簡単な例を用いながら説明する．
−昼食−
セッション３ 13:20-15:00 「UML設計への形式的手法の適用」
岸 知二（北陸先端大）
【講演概要】形式的検証をソフトウェア開発に適用するアプローチのひとつとして，UMLで表現されたソフトウェア設計の検証に適用する方法がある．UML設計へ形式的手法を適用するためには，UMLで表現されたの設計モデルやその上で確認したい性質を形式的検証の世界へマッピングする必要がある．本講演ではモデル検査技術によるUML設計検証を取り上げ，UML設計をどのようにモデル検査の世界に対応付けるのか，それによってどのような検証ができるのかを説明するとともに，UML設計検証を支援するツールを紹介する．
セッション４ 15:10-17:00 「組込みソフトウェアへの形式的手法の適用」
岸 知二（北陸先端大）
【講演概要】形式的手法は強力な技術であり，組込みソフトウェアの開発に適用することで従来のレビューやテストといった検証手法よりも，はるかに厳密で網羅性の高い検証効果を期待することができる．しかしながら，形式的手法は従来の検証技術よりも精密でナイーブな技術であるため，現実のソフトウェア開発に効果的に適用するためには，原理的な問題だけでなく，ソフトウェア工学的な観点から適用手法を検討することが不可欠である．本講演では，モデル検査技術を組込みソフトウェアの設計検証に適用した事例を題材に，上記の問題について具体的に説明する．