现代软硬件系统变得越来越复杂和智能化,并具有并发的特征。随着并发系统的广泛应用,尤其在关系人们生命财产安全的领域,其可靠性受到高度重视。传统的安全性保障方法主要基于测试技术,难以保证测试用例覆盖系统的所有可能执行路径。模型检测通过数学方法验证系统模型是否满足需求属性,具有完备性和自动化等优点,因而受到青睐。但是模型检测的建模过程通常由手工完成,因此对于并发系统,需要一种能够描述其行为和功能的建模语言。设计和应用针对并发系统的建模语言,其主要面临的问题有:(1)如何描述系统的控制流和数据流以及并发等特征;(2)如何减少建模的成本,提高建模的效率;(3)如何保证系统、模型、验证之间的一致性;(4)如何解决系统的白箱验证与保密性之间的冲突。针对这些问题,本文做出以下研究工作:?提出针对并发系统的形式化建模语言MCD,并给出了其语法、语义和形式化定义。MCD使用模块作为基本组件,定义层次事件自动机和功能块过程分别用于描述系统的控制流和数据流。层次事件自动机通过状态和变迁与功能块过程统一起来。各个层次事件自动机并发运行,通过共享变量和信道进行交互。基于形式化语法和语义可以对系统模型进行形式化验证和分析。?提出由MCD系统模型生成模型检测代码的算法。将层次事件自动机翻译生成线程,将功能块过程翻译生成内联函数。利用阻塞和随机选择机制实现模型的同步异步和不确定性。通过定义功能块优先级和端口变量解决数据流中带环的部分。此外还可以根据用户的需求和配置使用不同的优化策略以减小系统的状态空间和检测时间。?基于MCD建模语言设计实现了模块化建模与模型检测一体化平台M3C,该平台没有使用任何开源代码和第三方库,完全自主知识产权。M3C采用模块和图形化方式建模,自动生成模型的检测代码并进行模型检测,最后将检测结果以可视化的方式显示。还实现了语法检查,模块的自定义和复用等功能。M3C降低了形式化验证的使用门槛,同时提高了建模的正确性和效率。?使用M3C对列车通信网络中的实际系统进行了建模验证。经过验证发现系统存在缺陷,可能导致功能异常。通过和系统设计人员沟通合作,找到并修复了错误。证明了本文所提出的方法和工具的实用性。