软件的质量和可靠性问题由来己久。目前，虽然软件分析、设计和测试技术仍是保障软件可靠性的主要手段，但是由于人们对软件系统分布式处理，并发处理，实时处理等能力要求的日益增强，使软件系统正日益趋向高度的复杂化，导致上述方法仍然不能完全满足开发高可靠软件系统的需要。模型检测作为一种形式化验证技术因其严格的数学基础、全自动的验证过程，以及早期在硬件系统和协议验证中的成功应用而倍受学术界和产业界的关注。但是在软件工程各阶段中结合模型检测，全面、自动的分析和验证复杂信息系统的需求、设计及性能模型、提高软件的安全性和可靠性尚处于探索阶段。针对上述问题，论文在软件工程中结合形式化方法与模型检测技术，分别从需求分析层面、模型设计层面以及性能设计层面研究具有分布式、并发和实时行为特性的复杂信息系统形式化建模及验证技术：首先，对形式化方法及模型检测技术的相关研究进行了综述，阐述了复杂信息系统的行为特征，分析了复杂信息系统形式化建模及验证工作的重点与难点，总结了该领域存在的问题以及未来的研究方向。其次，为验证复杂信息系统需求模型设计的正确性，将复杂信息系统的软件需求划分为顶层需求和技术层面需求，使用面向行为的抽象方法将领域政策建模为系统的顶层需求模型，并用RSL对其进行形式化规约。为验证及细化顶层需求模型，本文通过定义RSL语法及语义的转换规则将顶层需求模型的RSL规约转换为Promela模型，将顶层需求的性质规约描述为时态逻辑公式，最后使用模型检测器SPIN自动验证顶层需求模型对性质规约的可满足性。再次，为验证复杂信息系统技术层面需求模型设计的正确性，首先用UML顺序图建模复杂信息系统的动态交互场景；针对UML顺序图模型缺乏精确的动态语义以及不能自动验证模型动态性质的问题，为UML顺序图定义迁移系统操作语义及其到Promela模型的转换规则，将顺序图模型的XMI描述文件的解析信息自动转换为Promela程序；最后，将建模系统需求的Promela程序和描述系统性质规约的线性时序逻辑公式作为模型检测器SPIN的输入，自动验证系统技术层面需求模型设计的正确性。第四，为验证复杂信息系统设计模型的正确性，以UML状态图为系统建模的主要工具，使用元组定义UML状态图的主要元素，从而给出一种状态图模型的中间表示形式将层次状态图转化为平面状态图；基于该中间表示形式定义状态图模型的操作语义，设计复杂信息系统设计模型到NuSMV输入模型的语义转换规则；基于转换规则以及设计模型的XMI文档解析信息实现设计模型到NuSMV输入模型的自动转换过程，并通过证明状态图的操作语义与转换得到的NuSMV输入模块的操作语义为互模拟等价关系证明转换过程的正确性；最后使用模型检测器NuSMV验证复杂信息系统设计模型对其性质规范的可满足性。最后，研究复杂信息系统实时性能设计的形式化验证技术，在需求分析过程中使用UML协作图建模系统的任务体系结构，描述当外部事件到达时系统内部事件和任务的激活顺序；用事件顺序分析方法为并发任务分配执行时间预算，将UML协作图扩展为实时协作图；基于实时协作图模型构建并发系统的时间自动机网络，并将其输入到模型检测工具UPPAAL执行自动验证。最后，总结论文工作，并提出了下一步的研究方向。