现今,计算机系统日趋复杂,对其进行有效的管理变得越来越困难。随着人们需要的日益增加,系统中会同时存在更多的应用软件,服务器,存储器等。要想有效的管理这些要素,确保可靠性,系统就需要具有自我管理的功能。2001年IBM公司提出了自动化计算(Autonomic Computing)的概念。自动化计算主要由几个核心组成,自我保护、自我优化、自我配置和自我恢复。自我保护,即系统能够保护自己,防止外界的恶意袭击；自我优化,即系统能够自动调度资源,以达到降低系统运行消耗的目的；自我配置,即系统配置能够自动完成,并能根据需要自动调整,来适应动态变化的运行环境；自我恢复,即系统能够自动从常规和意外的故障中恢复,正常继续运行。自动化计算系统通过严格的控制各个部分之间的交互来达到自治。但是构造,控制这些交互十分困难。如何开发一个具有高预测性的,安全可靠的IT系统呢?在这个问题上,我们可以运用严格的数学技术一一形式化方法。Communicating Sequential Processes (CSP)是一种形式化方法。其对模块间的通讯进行刻画,从而模拟整个系统的性质及行为。在描述分布式并发系统中,起到了很大的积极作用。本文以分布式声音识别系统(DMARF)为实例,从自保护,自优化,自恢复三个方面,利用CSP方法描述其自治性质,给出形式化自治需求规范。从而实现在分布式声音识别系统上,添加一个自治层,以达到减少维护系统的工作量的目的。在此基础上,运用Process Analysis Toolkit (PAT)工具,对自动化性质进行检验。