形式化方法主要包括两个方面:一是形式规约,二是设计验证,其本质是基于数学的方法来描述软件系统及其属性的一种技术,为软件的正确性与可靠性提供了前提条件,目前已经成为软件和硬件开发所必须的工具。模型检测作为一种自动检测技术,取得了广泛的应用,主要应用于计算机硬件、安全认证协议、通信协议、控制系统等方面的分析与验证等。本文所做的主要工作如下:(1)首先研究了结合数据性质的进程演算系统CCS-Z,并给出该系统的语法以及语义。语法主要由五大部分组成,其中包括输入动作、输出动作、内部动作、CCS部分以及Z部分。输入、输出和内部动作用于刻画系统的行为,CCS部分用于刻画系统的状态转换,而Z部分用来刻画系统内部变量的变化过程。语义部分给出了CCS-Z系统中五个算子的操作语义。该系统将形式规约语言Z和进程演算系统CCS结合起来,形成CCS-Z系统,该系统既可以描述并发系统,又可以很好的刻画数据性质。其次是给出了用来描述进程等价的互模拟定义以及性质,如:互模拟的等价关系以及同余等性质,包括强互模拟和弱互模拟两种,并给出这些性质的详细证明。(2)接着又给出了用来描述该系统的逻辑,该逻辑部分是用来描述系统的性质,包括逻辑公式以及可满足关系两部分。逻辑公式是用来刻画系统的性质,本文主要使用的逻辑系统是计算树逻辑CTL,在计算树逻辑中除了布尔连接词以外,还有十个基本算子,由于其他七个算子可以均可用EX、EU、EG算子表示,所以不再重复使用。可满足关系用来描述一个系统与其性质之间的一种关系,该部分给出了基本算子的可满足关系,其中包括原子命题、否定连接词、合取连接词、EX、EU、EG以及存在量词。(3)最后给出了模型检测部分,该部分给出了用于检测CCS-Z系统的模型检测算法以及实现该算法的类图和流程图。其中类图主要给出了算法实现过程中类与类之间的关系,而流程图则给出了该算法的执行过程,该部分也给出了开关控制系统以及火车控制系统的状态转换图。开关控制系统包括两个开关以及控制开关的控制器,在给出了该系统的输入信息以后,用公式描述系统性质的检测结果;火车控制系统包括左右两个火车以及通过红绿灯的控制系统,也给出了该系统的输入信息以及该系统性质的检测结果。