会議名 : 第3回STOC事例WG会合 場所 : （株）東芝本社ビル　30B10会議室 日時 : 20001/1/15　14:00〜18:00

参加者:(敬称略)
主査：塚本（東京工科大学）、副主査：五十嵐（東芝） 高田、本田（以上、豊橋技術科学大学）、南角（三菱電機）、福場（キャッツ）、 田村、荒木、山元（以上、東芝）、千星（STOC事務局：ソリトンシステムズ） 谷本、小林（記）（以上、日立製作所）

議事:

事例発表

1.VisualSpec - ZIPC開発事例（中間報告）：担当　キャッツ様
（内容）・VisualSpec-ZIPCのデモセットをとして携帯電話のMMI部を適用。本事例は、その 中間報告。詳しくは、発表資料参照（別途送付予定）
（開発の流れ）
　・デモセットの外部仕様よりVisualSpec設計、ZIPC設計、ターゲット・デバックを行う。
（ViualSpecの役割）
　・ビヘイビアツリーで概要設計。・Viual　Basicで動作検証。
（ZIPCの役割）
　・VisualSpecから変換したSTMを元に状態遷移の漏れを検証する。・RTOSを意識した実装を行い検証する。
（中間報告）
　・ViualSpecで作成した階層構造のビヘ−ビアツリーでは、ZIPCとの連携に問題あり。 ZIPCでは、拡張階層状態遷移（階層を飛び越えた遷移可能）があるが、SpecC、ViualSpecとも対応困難。
→　非階層構造は、VisualSpec-ZIPCの連携スムーズ。
（質疑応答）
　・イベントの扱いについて（豊橋工科大学）
　→　ZIPCでは、シーケンシャル、パラレルなイベント制御を実現している（send_msg）。 SpecCのイベント制御に関しては、言語WGで議論中。
　・ビヘ−ビアの遷移について（東芝）
　→　全ての状態遷移のチェックは、出来ない。ZIPCでは、入力された遷移に対して表形式でチェックできるのがメリット。

2.Rhapsody、SpecC適用に対する検討：担当　三菱電機様
（内容）
　UML→SpecC変換を考慮した適用を考えており、検討は、開始したばかりである。検討内容は、配布資料を参考のこと。 （結果）
　開始直後であるため、成果が出次第報告する。　なお、UML→SpecCへコンバートする際のルール、 SpecC vs Verilog-HDLの対応表を作成する予定。第一段として、 SpecC vs Verilog-HDL対応表を作成し、次回以降に報告する予定。

3.SIOによるSpecC評価：担当　豊橋工科大学様
（内容）
　SIOを使用し、HW/SWの区別の無いレベルの記述が可能であるか、SpecCを使用し、検証を行った。詳細は、配布資料参照。
（結果・質疑応答）
　・SpecCのセマンティクスについて
（１） notifyの仕様が不明確。また、Design Waveに記載されたチャネル記述に誤まりもある。
　　→　notifyについては、言語WGでも議論中。用途別のイベント制御が必要ではないか？
　　→ 次回、検討項目
（２） 並列動作は、waitfor(delta)を入れると動作が換わる。
　　→　waitfor(0)で回避できる。waitfor(delta)は、使用不可（東芝）
（３） try-trap構文を使用すると、VisualSpecで処理が停止する。
　　→　VisualSpecの不具合？
（４）その他、ViualSpecに関する問題は、バージョン1.3で対策済み。
　

言語WGからのお知らせ：担当　荒木
1.目的
（１） SpecCのセマンティクスの明確化
（２） Specチャートの図式表現
（３） 推奨するガイドラインの定義
2.SpecCリリーススケジュール
（１） バージョン1.0　…　現リリース版の不具合対策
　　　2001/01　 ：　STOC総会で承認
　　　2001/06 ：　リリース（イベント処理(notifyのイベントをためる)、import廃止、waitfo(delta)廃止等）
（２） バージョン2.0 …　言語WG、事例報告会の意見反映
　　　2001/06まで :　議論
2001/06〜08 : ドラフト
　　　2001/08　　 :　承認
　　　2001/10　　 :　STOCで承認
　　　2001/12？　 :　リファレンスマニュアル

その他
メーリングリストを開設した。自由に投稿ください。

次回開催予定
（１） 2/27（火）10:00〜　言語WGへの要望事項まとめ
今までの事例で指摘された項目を以下に案として纏めます。

i．計算モデルの見直し
拡張階層化状態遷移で取り扱っている項目を以下に記す。
　　　　１）階層をまたいだstate遷移
　　　　２）関数を遷移条件として利用可能
　　　　３）並列実行state-machine間で、互いの遷移条件が互いの状態(遷移)により影響し合える機構
上記を、現状のSpecCの計算モデルConcurrent SFSMD(Super State Finite State Machine with Data-path) に取り込むべきかの検討。即ち、構文要素の追加を行うべきか、SpecCイディオムとして扱うべきかの切り分け検討が必要。 この検討には、変換効率に対する配慮が必要。

ii．動的Semanticsの定義
現状のSpecCでは、ノンプリエンプティブなポーリングモデルを採用しており、 プリエンプション・ポイントをwait(0)で設定する仕様となっていると考えられるが、 この動作定義だけでは不十分だと考えられる。
プリエンプティブなポーリングモデルや、パラレルモデル、これら３つの融合等が考えられる。 サポートすべき動的Semanticsの分類と定義、及び夫々に必要な構文要素の抽出が必要。 勿論、変換処理系が認識可能なレベルでの、SpecCイディオムによる構文要素削減を行ってもよい。 （構文要素削減により、記述は可能だが変換処理において意味解釈が必要となり、 変換処理が困難になるような事があってはならない。）

iii．SpecCの計算モデル上でのSemanticsの定義
文法の直交性はそれほど重要ではなく、意味等価が認識できれば、変換規則等で、 syntactic variance(文法的多様性)の回避は可能。そのためには、明確な計算モデルの定義と、 代数的な意味定義が必要となる。

（２） ASP-DAC2001にモトローラ等海外メンバが来日する予定。都合合い次第、事例報告開催する。

以上