课程主页

 

课程论文题目(从未删除的题目中选择)

1.对Reo的模型检查有mCRL2和Vereofy两种方法，对它们进行深入比较和分析，讨论两种方法的优势和劣势。（1人）
2.开发将Reo语言转换到Promela的工具，考虑对某些连接件的性质使用SPIN进行模型检查，并将这一工作与mCRL2和Vereofy中的任一种进行比较。（2-3人合作）
3.使用Maude或Java/C/C++语言开发Reo量化模型关于QCTL的模型检查工具，并应用于一些实例。（2-3人合作）
4.扩充Reo设计模型的JTom或Maude实现，使得它可以描述实时Reo模型，并能够进行模型检查。（2-3人合作）
5. 开发将Chor&Role语言转换到mCRL2的工具，自己设计服务编排实例并使用相关工具对其性质进行模型检查，并与使用SPIN的模型检查进行比较。（2-3人合作）
6.开发将BPEL规范转换到Promela的工具，并使用SPIN对应用实例进行模型检查。（2-3人合作）
7.将UML状态机图或顺序图中的任一种转换到Promela或UPPAAL，设计应用实例并使用相应工具（SPIN或UPPAAL）检查模型的性质。（2-3人合作）
8.将WS-CDL转换到mCRL2，自己找一个应用实例，用mCRL2检查其性质并与相关工作进行比较。（2-3人合作）

课程论文要求

中英文均可，英文6000-8000字，中文8000-12000字。
结构清楚，重点明确，要有实例分析和相关工作比较，论文中不要用代码凑字数。重要核心算法放在附录中，参考文献明确给出。附录和参考文献不计入字数。
具体论文格式可参考报告论文。
选择题目2-8的同学每月简单报告一次进度。
也可以自己决定合适的研究课题，但所选题目需要符合讨论班主题宗旨，并与主讲老师讨论取得同意。自选题目需写一个研究建议，说明为什么该题目有研究意义，而且与讨论班有关，讨论之前通过email发给我。
抄袭（包括翻译）者一经发现成绩为0分。

　

相关材料

Reo: http://reo.project.cwi.nl
mCRL2: http://www.mcrl2.org/mcrl2/wiki/index.php/Home
Vereofy: http://www.vereofy.de/
WS-CDL: http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217/
UML: http://www.uml.org/
Maude: http://maude.cs.uiuc.edu/
Tom: http://tom.loria.fr/wiki/index.php5/Main_Page
SPIN: http://spinroot.com
CSP: http://www.usingcsp.com/cspbook.pdf
Chor语言是裘宗燕教授提出的一种描述服务编排的形式化语言，发表在WWW’07会议上。相关工作可见：
http://www.is.pku.edu.cn/~fmows/
Reo的量化模型和设计模型相关论文链接可在我的主页上找到:
http://www.math.pku.edu.cn/teachers/sunm/
参考材料中提供部分相关论文 。