在实时控制系统中，软件是控制反馈环的重要部分。该类软件中增加了严格的时间要求，同时低级的实时技术须与高级的程序设计、网络通信、仿真和控制相结合。作为控制大型复杂不确定系统的基础，系统构架分析就处于首要地位。目前，实时控制系统的构架分析主要依靠经验，并借助UML等建模工具。UML虽然可以给系统建立静态和动态模型，但是这些模型往往存在二义性，不能真正表述系统需求，并且在描述系统时间信息方面存在较大困难。 本课题的研究内容是将形式化方法CSP、B方法和OCL引入到实时控制系统的构架分析中。尽管CSP和B方法都是一种较好的形式化方法，可以用于系统构架分析。但是，单独一种在描述实时控制系统构架方面都存在不足，如CSP不擅长对数据和函数等进行定义，而B方法在描述系统并发控制等方面又存在局限。本文创造性的提出一种新的形式化方法CSP-B的设计策略。CSP-B是将形式化方法CSP和B方法集成在一起，集成后的CSP-B通过在规格中引入CSP来保持对系统的总体结构、控制能力及行为描述等方面的特性；通过引入B方法来实现抽象数据结构定义、系统限制以及功能处理等方面的特性。 本文介绍了通讯顺序进程(CSP)的符号系统，CSP是一种形式化方法，能严格地表述一个系统或进程执行事件的时序性以及系统之间相互通信的特性。本文也介绍了另一种形式化方法-B方法的形式化定义，B方法支持大部分的软件过程：需求分析、规格说明、软件设计、实现和维护等。同时，本文也给出了对象约束语言(OCL)的使用方法及形式化定义，OCL是一种对UML模型进行约束描述的形式化语言，允许开发人员创建模型中各个对象之间的详细约束规则。 为了验证CSP-B方法的有效性，本文将CSP-B运用到具体的实时控制系统的架构分析当中，从而得到CSP-B规格。由于目前没有支持CSP-B方法的有效工具，并且鉴于UML已经成为国内软件开发的事实工业标准，所以本文尝试将CSP-B规格用UML模型来表示。由于UML是非形式化的，其模型在某些方面有一定二义性，所以本文将UML模型添加OCL约束以消除模型的二义性。最后，本文借助类RTOS的实时控制系统框架ARTIC，以面向过程的C语言表示面向对象的思想，并使用MFC类实现了整个系统及测试。