近年実時間システムの提案が増えているが,このようなシステムの仕様は時間オートマトンなどで記述される. しかし時間オートマトンでは入力値などのデータを扱えないため仕様の記述が難しい場合がある. そこで我々は時間オートマトンモデルを入出力データが扱えるように拡張したデータ付時間オートマトンモデルを提案した.また双模倣等価性を機械的に判定するアルゴリズムを考案し,現在実装に取り組んでいる. 本発表ではデータ付時間オートマトンについて説明するとともに,実装の現状及び今後の課題について述べる.
Back