O desenvolvimento de software de sistemas de controle pode ser caracterizado como um trabalho de alta complexidade. A sua alta complexidade se deve principalmente às características de não determinismo, assincronismo e concorrência entre os seus processos. Este trabalho propõe uma nova arquitetura de sistemas de controle baseada em padrões de projeto e na utilização da combinação de linguagens de especificações formais CSP e Object-Z (CSP-OZ). A linguagem Object-Z é utilizada para se especificar características estáticas e métodos de classes através da utilização de predicados, enquanto que CSP é uma álgebra de processos utilizada para especificar a dinâmica de processos concorrentes. A proposta desta arquitetura visa a construção de uma arquitetura robusta, correta, de fácil modificação, reutilizável e que possa servir de base para implementação de projetos futuros. A arquitetura do software é dividida em duas partes. Na primeira parte, alguns padrões de projeto comumente utilizados em sistemas de controle são especificados utilizando-se a linguagem de especificação formal CSP-OZ. As especificações formais são convertidas em programas JAVA através da utilização da biblioteca JCSP (uma biblioteca construída para traduzir facilmente especificações CSP). Na segunda parte, as aplicações utilizando CSP-OZ e JCSP são construídas baseadas em uma biblioteca de padrões de projeto que foram previamente analisadas. Um estudo de caso é utilizado para se testar e validar a arquitetura proposta

The development of control system software might be characterized as a highly complex task. This is mainly due to the characteristics of nondeterminism, asynchronicity and concurrency between processes. In this work, a new control system architecture based on design patterns and the use of a combination of formal specification languages CSP and Object-Z (CSP-OZ) is proposed. Object-Z can specify the state space and methods of a class using predicates while the CSP is a process algebra that can specify the dynamics of concurrent processes. The proposal aims at designing a robust, provable, maintainable and reusable architecture that can serve as a base of future project implementations. The software architecture is designed in two parts. In the first part, some design patterns which are commonly used for control systems are specified using CSP-OZ formal specification language. These formal specifications are converted into JAVA programs using the JCSP library, a software library designed to easily translate CSP specifications. In the second part, applications using CSP-OZ and JCSP might be designed based on the library of design patterns that are previously provable correct. A case study is used to test and validate the proposed architecture.