早期需求工程中的形式化建模与模型检验应用研究

摘要	第1-4页
ABSTRACT	第4-6页
目录	第6-7页
第一章 绪论	第7-10页
·论文的背景	第7-8页
·本文研究工作	第8-9页
·文章组织	第9-10页
第二章 基本理论与相关技术	第10-22页
·需求工程	第10-11页
·早期需求与i*角色标记建模和 GRL建模语言	第11-16页
·形式化方法和模型检查	第16-18页
·模型检查工具Nusmv	第18-21页
·本章小结	第21-22页
第三章 将早期建模应用于网上教学系统中	第22-31页
·网上教育系统的体系结构	第22-24页
·根据网上教学体统特点建立模型	第24-29页
·本章小结	第29-31页
第四章 模型形式化语言描述的生成技术	第31-43页
·和I*相对应的形式化描述	第31-37页
·图形化描述到形式化语言的框架自动生成	第37-42页
·本章小结	第42-43页
第五章 模型形式化描述向NuSMV验证语言的转化	第43-59页
·形式化描述语言向Smv语言的转换	第43-48页
·一个模型检查实例分析的例子	第48-58页
·本章小结	第58-59页
第六章 结论与展望	第59-64页
·总结	第59页
·展望	第59-64页
参考文献	第64-67页
致谢	第67-68页
攻读硕士学位期间发表的学术论文	第68页