【作業全体の説明】

甲南大学知能情報学部のソフトウェア設計検証研究室です．
この度は私共の実験にご協力頂きまして誠にありがとうございます．

これから取り組んでいただくのは，Alloy と DTRAM と呼ばれる2つの仕様記述言語による仕様記述の読解，仕様記述に関する設問への解答，およびアンケートへの回答です．
全体の作業時間としては，3~5時間程度を想定しています．Alloy および DTRAM の説明，仕様記述言語全般の解説などは実験の中で行います．
仕様記述の対象となるシステムは2つあり，それぞれのシステムについて，Alloy による仕様記述と DTRAM による仕様記述を読んでいただき課題に取り組んでいただきます．
したがって，取り組んでいただく課題は計4つになります．それぞれのシステムの仕様は小さく，そのため仕様記述の行数も多くはありません．
これらの課題は，すべてWeb上で行っていただくことができます．課題を終えるたびに，設問およびアンケートにお答えいただきます．
これ以降お答えいただく設問およびアンケートは，課題毎に3つ，対象システム毎に1つ，すべての課題の終了後に1つの計15個です．
設問およびアンケートの数は多いですが，1つ1つの質問項目は多くありません．課題が終わるたびに作業を中断していただいて構いません．

実験の流れ：

実験は以下の流れで行います．

  1. 実験用のWebページ(本ページ)にアクセスしていただきます．
  2. Alloy の概要を説明します．
  3. 1つ目のシステムである酒屋の在庫管理システムの仕様を説明します．
  4. 1つ目の課題に取り組んでいただきます．
  5. DTRAM の概要を説明します．
  6. 2つ目の課題に取り組んでいただきます．
  7. 酒屋の在庫管理システムに関するアンケートにお答えいただきます．
  8. 2つ目のシステムであるツイートシステムの仕様を説明します．
  9. 3つ目の課題に取り組んでいただきます．
  10. 4つ目の課題に取り組んでいただきます．
  11. ツイートシステムに関するアンケートにお答えいただきます．
  12. 最後に実験全体に関するアンケートにお答えいただきます．


【Alloyの説明】へ