Modeling and analysis of hybrid supervisory systems.

Author(s)

Emília Villani

• Document type: Doctoral Thesis
• Press: São Paulo. , gráficos, ilustrações, tabelas.
• Institution: Universidade de São Paulo (USP). Escola Politécnica (EP/BC)
• Defense date: 2004-03-04

Examining board members

Paulo Eigi Miyagi; Reginaldo Arakaki; Stéphane Julia; Arthur Jose Vieira Porto; Robert Jean Valette

• Advisor: Paulo Eigi Miyagi
• Field of knowledge: Engineering - Mechanical Engineering
• Indexed in: Banco de Dados Bibliográficos da USP-DEDALUS; Biblioteca Digital de Teses e Dissertações - USP
• Location: Universidade de São Paulo. Biblioteca Central da Escola Politécnica; EPBC/FT-1948; Universidade de São Paulo. Escola Politécnica. Biblioteca de Engenharia Mecânica, Naval e Oceânica; EPMN/FT-1948

Abstract

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. (AU)