Modelagem de sistemas químicos como máquinas de estados finitos para fins de verificação formal [recurso eletrônico]
TESE
Português
T/UNICAMP C65m
[Modeling of chemical process systems as finite state machines for formal verification]
Campinas, SP : [s.n.], 2018.
1 recurso online (140 p.) : il., digital, arquivo PDF.
Orientador: Roger Josef Zemp
Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Química
Resumo: A análise da segurança de processos industriais é feita primariamente com ferramentas como HAZOP e Análise de Árvore de Falhas. Esses métodos exigem conhecimentos de diversas áreas e contam com a participação de engenheiros e outros profissionais na elaboração de documentos que descrevem...
Resumo: A análise da segurança de processos industriais é feita primariamente com ferramentas como HAZOP e Análise de Árvore de Falhas. Esses métodos exigem conhecimentos de diversas áreas e contam com a participação de engenheiros e outros profissionais na elaboração de documentos que descrevem cenários de desastre e planos de contingência. A modelagem e simulação de processos poderia ser usada nesse sentido para auxiliar na determinação de condições operacionais que levariam ao desastre. Porém, explorar todo o espaço de estados do modelo de um processo em busca destes cenários é custoso, e frequentemente inviável, em termos de tempo computacional, pois os cenários a considerar são, usualmente, infinitos. Para resolver problemas exploratórios semelhantes, cientistas da computação desenvolveram métodos para deduzir se modelos de sistemas físicos atendem ou não certas propriedades (um programa nunca pode travar ou um processador nunca pode errar os cálculos, por exemplo). Esse conjunto de métodos, chamado de verificação formal, em geral exige modelos que os engenheiros químicos não estão acostumados a trabalhar, como as máquinas de estados finitos. Assim, o presente trabalho teve por objetivo o desenvolvimento de um método para modelagem de processos químicos como máquinas de estados finitos para que estes modelos pudessem ser utilizados em verificação formal. O método extrai informações sobre a dinâmica do processo e constrói automaticamente as máquinas. O método foi aplicado em um estudo de caso de um reator CSTR com múltiplos estados estacionários, onde o modelo resultante foi verificado a fim de descobrir rotas de partida do equipamento e alcançabilidade dos estados estacionários em termos das variáveis operacionais disponíveis. A técnica se mostrou eficaz e flexível o suficiente para construir a máquina a partir de diferentes fontes de informação da dinâmica do processo, inclusive, em princípio, de simuladores de processos
Abstract: HAZOP and Fault Tree Analysis are generally used as tools for industrial safety analysis and they usually require knowledge from several different areas. Engineers and other professionals use those tools to develop documents describing hazard scenarios and contingency plans. Process...
Abstract: HAZOP and Fault Tree Analysis are generally used as tools for industrial safety analysis and they usually require knowledge from several different areas. Engineers and other professionals use those tools to develop documents describing hazard scenarios and contingency plans. Process modelling and simulation could help during the elaboration of this documentation by indicating operational conditions with potential to disaster. However, exhaustive exploration of the model state space to search for these scenarios is very time consuming, and frequently impracticable, because the considered scenarios are, usually, infinite. To solve similar exploratory problems, computer scientists developed several methods to prove if models of physical systems meet some specifications (e.g. a software must not have deadlock or a CPU must not miss any operation). These methods, called formal verification, sometimes require models that chemical engineers do not usually deal with, like finite state machines. This work aimed at the development of a method to model chemical processes as finite state machines for formal verification purposes. The method extracts information about the system's dynamics and builds automatically the machines. The technique was applied on a case study of a multiple steady state CSTR, where the finite state model was verified in order to find viable startup strategies and analyze reachability of stable steady states with the available operational variables. It was demonstrated that the method is effective and flexible enough to build the machines from serveral different sources of information of the process dynamics, including, in principal, from process simulators
Requisitos do sistema: Software para leitura de arquivo em PDF