软件需求分析是整个软件开发过程中极为重要的环节，它不仅仅是技术问题，也涉及了组织、管理、商务、社会等问题。在早期的需求分析过程中，描述建立了软件系统的动机、意向和原则，使得开发能更好地理解组织关系和活动者的依赖关系，明确各种决策的原则；解决意向系统如何满足组织的目标，为什么需要这样的系统，有什么替代方法可以考虑，替代方法对用户的影响，用户的兴趣如何满足等。早期需求的另一个重要特性就是获取系统的非功能需求(即软目标)，即质量属性，如精确性、性能、安全性、可调整性等。所以在早期需求开发中如能发现系统的潜在问题将比在后期开发中花费在解决所暴露的问题节省数百倍的开销。 我们针对网上教学系统的特点对其进行早期的需求分析。提取了系统主要角色细化分析了他们的意图、任务、资源依赖。然后用图形化的方法对我们的分析进行了呈现，建立了系统的事务模型。通过程序的自动翻译图形化表示的记录文件生成了相对应的模型形式化表示的语言框架代码描述。经过手工加入更多的模态逻辑指定后形成了系统完整的形式化语言描述的模型。为实现模型检查我们采用了NuSMV模型检查工具，并将前面所建立的模型形式化语言描述转换为NuSMV模型检查工具可以接受的脚本语言从而实现了对我们对模型的检查过程。根据检查的结果一步步调整修改逻辑关系和指定，最后得出趋向于反应系统真实情况的形式化模型表述，并在论文的附录中给出了相应的结果和我们建立的模型。