機構解析ツールを開発している韓国ファンクションベイ社と共同で、メカとソフトの協調設計、検証の可能性を調査するプロジェクトを開始いたしました。ファンクションベイ社の機構解析ツール「RecurDyn」と「ZIPC」を接続ツールを介して協調動作させ、RecurDyn上のメカモデルをZIPCで制御することができます。 これにより、実機ができる前に、ソフトがメカの異常に妥当に対応しているかを検証することができ、製品の品質向上に役立てることができます。

組込みソフトウェア研究として、CESLでは、形式手法研究、具体的には、リソーススケジューリング検証技術の研究、車載組込みソフトウェア向け状態遷移表モデル検査技術の研究などを行なっています。

形式手法は、ソフトウェアの数学モデルを構築する技術と、その数学モデル上で指定した性質が成り立つかどうかを検証する技術の総称です。数学モデルの例として、状態遷移表があり、指定する性質の例として、「不可セルに到達しないこと」、「変数xの値が常に10以下であること」があります。

リソーススケジューリングとは、ネットワークやバス上に分散したタスクが、時間制約を守りながら、競合せずに共有リソースを使用できるようにする、スケジューリングのことです。タスクは、マルチキャスト通信をしながら処理を実行しますが、ネットワークやバスにはメッセージ遅れがあるので、各タスクが時間制約を満たしながら、競合せずに共有リソースを使用していることを検証するのは、簡単な作業ではありません。この「分散したタスクが、時間制約を守りながら、競合せずに共有リソースを使用していること」を検証する技術（リソーススケジューリング検証技術）を研究しています。

リソーススケジューリング検証では、数学モデルとして、図1のようなリソーススケジュール図を用います。リソーススケジュール図には、タスクがいつリソースを使用し、いつマルチキャスト通信をするかを記述します。図1には、T1、T2、T3の３レーンがありますが、これらは、それぞれタスクT1、T2、T3の動作記述に対応します。リソーススケジュール図の各レーン上の右矢印は、タスクがリソースの確保を待っていることを意味し、白箱は、タスクがリソースを確保していることを意味します。ここでタスクT1の時間制約を、「最大300ms毎に、24msリソースを確保する」とします。T1レーンは、「タスクT1は、84ms待った後、24msリソースを確保し、180ms待つ」の繰り返しという動作記述で、時間制約を満たす動作の一つです。リソーススケジュール図のレーン間の矢印は、マルチキャスト通信を意味します。図1のC_T1_T2、C_T1_T3は、T1からT2、T3へのマルチキャスト通信を意味します。C_T1_T2下の0..58はメッセージ遅れの制約を記述しており、T1からT2へのメッセージは、0msから58msの間に到達することを意味します。

リソーススケジューリング検証では、モデル検査ツールUPPAALを利用します。リソーススケジュール図をUPPAALのモデルに変換し、検証する性質に対応するUPPAALの検証式を与えて検証を行います。図 1のうち、タスクT1に関する部分は、図 2のUPPAALモデルに変換します。「タスクT1は、最大300ms毎にリソースを確保する」は、
　　　A[] t1.clck <= 300
というUPPAALの検証式を与えて検証を行います。

2007年度から始まった知的クラスター創成事業（第�U期）に、共同研究企業として参加しています。「車載組込みソフトウェア向け状態遷移表モデル検査技術の研究開発」をテーマに、九州大学、ふくおかISTと共に研究を進めています。