Q: ルール適用順序は静的に決まるのか？
A: 式の形で判断するので、静的に決まる。ただし、式の形の処理が 困難なので、自動化は困難。モデルチェッキングはガード付き遷 移に対応していないので、ガードを除去すると状態数が増える問 題がある。そのため、モデルチェッキングによる検証と、テスト の併用を考えている。
Q: 対象は？
A: まだ限定していない。照明制御、大きいものでは携帯電話など
Q: プリンタ、スキャナなどで、ゼロから作ることはありえない。
A: それは重要なポイントである。製品ラインに着目して仕様を整理 すれば、仕様の再利用ができるので、仕様を体系化する研究が存 在し得る。
Q: モデルチェッキングの具体的な処理系は？
A: ヨーロッパにあるようなので、調査中。昔よりはマシンの性能が 向上しているので、以前は不可能なチェックも可能になっている。
Q: データ構造とイベントを組み合わせるということはどういうことか？
A: ルールの条件中でデータ構造のデータを引用。 アクションでデータを更新する。
Q: 通常のグローバル変数がデータ構造に置き換えるのか？
A: Yes
Q: 非正常系の対策にはソフトウェアのバグや、ハードウェアの素材の 劣化を含むか？
A: 外部のソフトウェアモジュールのバグには、入力のチェックで 対応できよう。ハードウェアについては、ソフトで経年劣化に 対応している例は現実にある。
Atsushi Ohnishi
2003-06-12