Sistemas Supervisórios Híbridos podem ser definidos como sistemas de controle cujos estados são representados por variáveis discretas e contínuas, e cuja dinâmica é determinada em função do tempo e da ocorrência de eventos discretos. O desenvolvimento desta classe de Sistemas Supervisórios pode ser dividido em duas fases. A 1ª Fase consiste na elaboração de um modelo protótipo para o Sistema Supervisório, que é descrito usando um formalismo, e que é validado com base nas especificações do problema. Na 2ª Fase, este modelo, já validado, é convertido na linguagem de programação do Sistema Supervisório propriamente dito. Esta tese concentra-se na 1ª Fase, para qual abordam-se três questões principais: (1) a escolha do formalismo de modelagem; (2) como construir o modelo do Sistema Supervisório Híbrido usando este formalismo; e (3) como validar o Sistema Supervisório Híbrido usando o modelo construído. Para questão (1), introduz-se um novo formalismo de modelagem baseado na aplicação dos conceitos de Orientação a Objetos (OO) às redes Predicado Transição Diferenciais (redes PTD). Este novo formalismo é chamado de redes PTD-OO. No que se refere a questão (2), é proposto um procedimento para obtenção do modelo do Sistema Supervisório em redes PTD-OO usando os diagramas da UML (‘Unified Modeling Language’). Finalmente, para a questão (3), o problema de validação é abordado através da definição de um conjunto de propriedades que o modelo em redes PTD-OO deve respeitar afim de que sejam garantidos os requisitos do Sistema Supervisório. Estas propriedades são, então, verificadas através de um procedimento proposto para análise de redes PTD-OO.

Hybrid Supervisory Systems can be described as control systems with states that are represented by both discrete and continuous variables. Their dynamics are function of time and depend also on the occurrence of discrete events. The development of Hybrid Supervisory Systems can be divided in two phases. In the 1st Phase, a prototype-model for the Supervisory System is described using a specific formalism and is validated based on the system requirements. In the 2nd Phase, this validated model is converted to the programming language of the Supervisory System. This thesis is focused on the 1st Phase of Hybrid Supervisory System development. It approaches three main issues: (1) the choice of the modelling formalism; (2) how to build the Hybrid Supervisory System model using this formalism; and (3) how to validate the Hybrid Supervisory System using this model. For issue (1), a new modelling formalism is introduced based on Differential Predicate Transition nets (DPT nets) and object-oriented (OO) paradigm. This new formalism is called DPT-OO net. Then, for the issue (2), a modelling procedure that assists the building of the DPT-OO net model using Unified Modelling Language (UML) diagrams is proposed. Finally, for the issue (3), the validation problem is approached by defining a set of properties of the DPT-OO net model that assures the Supervisory System requirements. These properties are then formally verified using a proposed analysis procedure.