1. Integrated method for designing complex cyber-physical systems
- Author
-
Gonçalves, Fernando Silvano, Universidade Federal de Santa Catarina, and Becker, Leandro Buss
- Subjects
Aeronave não tripulada ,Engenharia de sistemas ,Automação - Abstract
Tese (doutorado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2018. O projeto de sistemas ciberfísicos (CPS) é considerado uma atividade complexa, sendo composto por diferentes fases, essenciais para sua concepção. Neste sentido, a definição detalhada das fases de projeto se faz necessária, visando facilitar o projeto das aplicações e auxiliar na representação das suas características. Algumas dessas fases têm ampla discussão por parte da comunidade da engenharia, tais como o desenvolvimento dos sistemas de controle, por exemplo. Outras, no entanto, têm um menor grau de detalhamento, ou seja, as atividades que devem ser desenvolvidas não são amplamente discutidas ou detalhadas, dificultando a sua aplicação. Dentre estas temos a especificação dos subsistemas de sensoriamento e atuação, integração de processos de verificação formal, entre outras. Essas etapas, apesar de menos discutidas, também são essenciais no escopo do desenvolvimento dos CPS, pois suportam a especificação e validação de propriedades das aplicações, assim como são responsáveis pela integração da aplicação com o ambiente de atuação. No projeto dos CPS, um número considerável de métodos de desenvolvimento está disponível na literatura, visando guiar os desenvolvedores nas tarefas de modelagem, porém eles não apresentam adequado nível de detalhamento para as atividades supracitadas. Nesse contexto, este trabalho propõe o desenvolvimento de um método integrado que auxilie no processo de modelagem e integração dos CPS, mais especificamente dos Veículos Aéreos Não Tripulados (VANTs). O método proposto busca integrar os processos de modelagem funcional, de arquitetura, integração de sensores e atuadores e verificação formal, contribuindo no projeto do sistema embarcado, bem como na interface com o conjunto de sensores e atuadores, culminando, consequentemente, na construção das aplicações. O método proposto é baseado na engenharia dirigida a modelos (MDE) e sua abordagem busca permitir a construção automatizada dos modelos, garantindo a manutenção das características da aplicação durante todo o processo de desenvolvimento, permitindo a integração dos modelos gerados e auxiliando na validação das propriedades do sistema. Aliadas ao método proposto, duas ferramentas foram desenvolvidas, denominadas ECPSModeling e ECPSVerifier. Estas têm por objetivo dar suporte ao processo de desenvolvimento. O ECPSModeling opera na transformação do modelo funcional para o modelo de arquitetura, permitindo a integração das características de sensores e atuadores. Já o ECPSVerifier atua na extração do comportamento do sistema, transformando o modelo de arquitetura em um modelo de comportamento representado por autômatos temporizados, permitindo a aplicação da técnica de verificação formal model checking. Visando detalhar o método proposto e as ferramentas desenvolvidas, esses são aplicados ao projeto de um VANT birotor na configuração Tilt-rotor. Dessa forma, objetiva-se municiar o processo de desenvolvimento dos CPS, em especial dos VANTs, descrevendo suas principais fases de desenvolvimento. Abstract : The design of a Cyber-Physical System (CPS) is defined as a complex activity, being composed of a set of design phases devoted to model application characteristics. In this sense, detailing the phase characteristics is required in order to help the design teams during the project design, and to aim the support of the correct application characteristics representation. However, despite some of these phases, such as the control systems design, being discussed at length by the engineering community, other phases have less detailed studies, i.e., the design activities that compose these phases are not so well documented. In these sense, it is required more experience from the design teams to perform activities such as, the sensing and actuation subsystems representation, and the integration of formal verification methods on the design process, among others. Despite the lack of information related to them, these phases are essential to the CPS design, by the fact that they support application characteristics representation and the properties validation, as well as, they also provide the integration between designed system and their environment. Regarding the CPS design process, different methods are available in the literature, aiming to guide the designers to perform the modeling tasks. However, these approaches do not provide enough information related to those described activities. In this context, this thesis proposes an integrated method applied to CPS design, more specifically devoted to the Unmanned Aerial Vehicles (UAV) design. That proposed method aims to integrate different modeling processes such as functional, architectural, sensor and actuator integrations, and formal verification design processes. Based on the proposed activities this method aims to support the UAV embedded system design, and allow the integration between the embedded platform and the set of system devices. The Model Driven Engineering (MDE) is used as basis to the proposed approach, and aims to support the automated model generation based on the application characteristics. It is intended to ensure the maintainability of the system information over all the design steps and provide the property evaluation and validation, considering the model transformation principles. Two different tools are designed with the proposed method, the ECPSModeling and the ECPSVerifier, for supporting the design activities. The ECPSModeling provides the transformation process from functional model to architectural model, in order to integrate sensor and actuator characteristics. On the other hand, the ECPSVerifier provides the CPS behavior representation, based on the architectural model, by using timed automatas, which allows the formal verification evaluation by performing model checking. The proposed method and the designed tools are applied on the project of a tilt-rotor UAV design. The details of the method proposed in this thesis are demonstrated by performing the UAV project, described as a case study.
- Published
- 2018