その１

• UMLの分析からeMSCの設計データまで落とす過程を組織的にできないか?
  • PLUSの手法との結合の整理はレポートでおこなったが、中途半端だし、納得できない
  • サブシステム構造か（MSの抽出)とタスク構造化の裏のモデルがない。
  • なにかモデルがあって、このうえで、説明できないか？

その２

• PSL,モデルチェックがどのように上流設計で整理できるのか？
  • モデルチェックとPSLの対象の違いはなにか？
  • eMSCでモデルチェックな何に役に立つのか？
  • PSLとモデルチェックを組合せてなにか、設計手法はつくれるか？
  • Taharさんof HVG@Univ. Concordiaが詳しい
    • Assertion and Model Checking Assertion and Model Checking of SystemC
    • Design for Verification of a PCI Bus in SystemC
    • Modeling and Verification of DSP Designs in HOL
  • Design for Verification of SystemC Transaction Level Models

UMLでモデルと制約(PSL)を入力、モデルはASMに変換し、制約もPSLのASMセマンティクスにしたがって展開。
ASMにおちれば、モデルチェッキングすることができる。
そこで、状態爆発が起きれば、しょうがないので、モデルをSystemCに、PSLをモニターに展開して。アサーションの世界でかたをつける。

→ということは、ASMの世界だけでは片づかないクラスがあるということ。これはなに？

PSL自体はセマンティクスをHOLでかくとかあるみたい。

その３

• 抽象度の高い、（計算）モデルとしてASM(L)はどう活用できるのか？
  • IMRの中間言語として？？
  • 言語定義をして、コンバージョンをかけるセマンティクスエンジンとして？
  • モデルチェックするためのモデルとして？
  • その１のモデルとしてかける？？

その４

• システムモデルはなんなの？
  • 操作可能性
  • 検査可能性
  • UMLとの接続