|
無線を用いて各センサノードにプログラムをロードすることで、その動作を再定義可能な無線センサネットワーク: Reconfigurable Sensor Networkを実現した。センサノード動作を記述する専用言語Funclet+を設け、その記述から、形式検証ツールへの入力記述と、C言語記述を生成するトランスレータを開発した。形式検証ツールで生成された入力記述が動作検証された場合、生成されたＣ言語記述は正しく仕様を実現していることを保証できる。いくつかの典型的なセンサノードの動作を専用言語で記述し、形式検証ツールで検証した後、生成されたC言語記述が実機センサノードで正しく動作することを確認した。
|
