在计算机系统应用研究过程中,为了避免由微小差错而引发的损失,这些系统在投入使用之前,需要根据系统属性进行建模,并对建好的模型进行分析与验证,以保证系统投入使用之前系统功能方面的健壮性。模型检测是一种以数学为基础的形式化验证方法,为计算机系统的属性验证、系统研发、系统的修改和维护等提供了方便。本文对模型检测方法和相关理论进行研究,并将其应用于系统的形式化建模与属性验证中。相对于一般的实时系统,对系统的安全性有着更高要求的是一种以安全性为最高性能的计算机控制系统。这种系统一般包括离散行为,还包含具有时间约束的连续行为。在系统开发和建模的过程中,目前较为流行的建模方法是采用半形式化的统一建模语言UML与具有时间元素的时间自动机来建模。本文所做的主要贡献包含如下几方面:(1)计算机铁路车站联锁系统对系统的安全性要求极高,本文对该系统中的基本进路建立子模块进行研究,提出基于多个UML组合场景分析的系统形式化建模方法。该方法首先采用OCL前置和后置条件分析的方法对多个组合的UML时序场景进行分析,检测出场景中存在的矛盾行为并进行矛盾消解,得到一致的多组合UML时序场景,然后将一致场景中对象交互的行为序列转换成有限状态进程代数模型,在模型检测工具中进行组合操作,得到系统的形式化模型。该方法为安全苛求系统软件的需求分析与设计研究提供了新思路,为系统的形式化建模与验证分析提供了较好的解决方案。(2)本文提出了以时间自动机为基础理论,对物联网系统组合服务的建模方法,在基于物联网原子服务的基础上,对传统的时间自动机进行了一些扩展,将扩展后的时间自动机模型运用到物联网原子服务建模和组合服务的分层建模中去,根据原子服务中的原子个体特有属性的分析,采用UPPAAL工具对所建模型进行验证分析。本文先从微观角度对系统中的独立个体进行分析与建模,然后再从宏观的角度,将各单独的个体通过相关性连接在一起使其成为一个完整的系统,既有利于把握单个个体的独特性,又考虑了系统整体的连通性。通过本文的研究,针对不同的系统,分析不同系统的属性要求,对不同系统有针对性的建模,提高了系统建模的正确率,降低了软件开发与维护成本。通过研究实例,证明了本文提出的方法具有较好的实际可行性。