［研究グループ構成］
研究者：深谷健一，菊地慶仁
共同研究者：岸浪建史（北大），金井理（北大）
［研究課題と成果概要］
� 痢＿菫�情報処理の人間・移動ロボット連携作業への応用（深谷健一） ］
移動ロボットに荷物運搬や道案内などのサービスを実行させるとき，リアルタイムの画像情報処理技術を活用したコミュニケーション手段を提供することにより，スムーズなサービス実現に寄与する．ロボットと人間とのコミュニケーション手段として，人間が手に持って作業の種類と目標のボタンを押下すると，対応するRGBの発光ダイオード（LED）が点灯し，さらに装置自体を動かすことで方向などを示す装置を想定している．移動ロボットは搭載したリアルタイム画像処理装置でLEDの色と装置の動きを検出することで人間からの指示を検出してそれに対応する行動をおこなう．今年度はRGBの発光ダイオードの色識別がカラーフィルタ処理で可能なことを確認した．次年度以降，装置・ロボット間の画像表示のプロトコル設定，人間に使いやすくロボットから識別しやすい装置形状の検討を進め，入力ボタン，LED表示，マイコン，電源からなる装置を試作しその有効性を実証していく．
�◆痢．泪襯船瓮妊�ア機器入出力仕様の代数的記述方式と実装技術の確立（菊地慶仁） ］
情報機器開発の初期段階では，機器の設計仕様を表現する技術が確立されておらず，また製品仕様書もWordで書かれた文書がそのまま用いられていることが多い点が問題となっている．このため，本研究では，設計初期段階におけるシステムの入出力関係や状態遷移規則を形式的に記述し，挙動の安定性や操作性などを分析することを目的としている．
本年度は，まず代数的な仕様記述と公理系に基づいた検証方式の基本的な提案を行った．本報告で用いる方法論は公理によって表明を導出し，様々な目的の検証を行う方式である．計算機言語PascalのためにHoareが提唱した．
またMathematicaを用いて提案した方式に基づく試作システムを開発し，以下の基本的な性質の検証が行えることを示した．
1) 完全性
2) 強連結性
3) 状態数の最小性
4) 状態遷移の決定性
これらの成果は，北海学園大学工学部研究報告で発表した．今後は，より具体的なシステムを対象として，階層化された状態遷移，並行動作の仕様表現方法と検証について拡張していく必要がある．