Framework para modelagem e verificação formal de programas de controle de sistemas instrumentados de segurança (2014)
- Authors:
- Autor USP: FERRAREZI, RODRIGO CÉSAR - EP
- Unidade: EP
- Sigla do Departamento: PMR
- Subjects: FRAMEWORKS; SISTEMAS DE CONTROLE
- Language: Português
- Abstract: Devido à alta complexidade dos Sistemas Produtivos, o projeto de sistemas de controle adequados às exigências normativas vinculadas aos processos industriais que são executados, e seu impacto no ser humano e no ambiente demandam a necessidade do desenvolvimento de soluções de controle que sejam seguras e estáveis no sentido de não causar interrupções no processo produtivo e danos ao ser humano e ao meio. Uma abordagem para o desenvolvimento de sistemas que contemplem estes requisitos baseia-se no conceito de Sistemas Instrumentados de Segurança e na aplicação das normas IEC 61508 e IEC 61511. Entretanto, assim como o desenvolvimento de qualquer software, os programas de controle de SIS também estão sujeitos a erros de especificação e projeto, mesmo quando o desenvolvimento é feito conforme os critérios normatizados. Além dos erros de projeto, também deve ser levado em consideração que as camadas de prevenção e mitigação especificadas nas normas podem ser desenvolvidas separadamente e dessa forma podem ocorrer comportamentos não previstos ou indesejáveis quando da operação conjunta delas. Uma das formas para uma melhoria na confiabilidade desses programas e que também é um requerimento pertinente ao ciclo de desenvolvimento de um SIS - de acordo com as normas de segurança IEC 61508 e IEC 61511 - é a aplicação de técnicas de verificação formal dos modelos desses programas de controle bem como o uso de um ambiente unificado para modelagem desses sistemas de controle, onde suas interações possam ser mais bem compreendidas. Atualmente, umas das técnicas mais proeminentes para a verificação de sistemas é o Model Checking, que realiza uma busca exaustiva no espaço de estados de um sistema dirigido por eventos, verificando as propriedades especificadas a partir de proposições estabelecidas em lógica temporal.Para esse trabalho é utilizada a lógica TCTL devido a sua capacidade de expressar propriedades em domínio temporal denso. Como ferramenta computacional será usado o ambiente GHENeSys, que propicia um ambiente unificado para modelagem, simulação e verificação dos sistemas por conjugar os benefícios de rede de Petri para modelagem e as técnicas de Model Checking para verificação de modelos.
- Imprenta:
- Data da defesa: 09.12.2014
-
ABNT
FERRAREZI, Rodrigo Cesar. Framework para modelagem e verificação formal de programas de controle de sistemas instrumentados de segurança. 2014. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2014. Disponível em: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-31122015-112539/. Acesso em: 19 abr. 2024. -
APA
Ferrarezi, R. C. (2014). Framework para modelagem e verificação formal de programas de controle de sistemas instrumentados de segurança (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/3/3152/tde-31122015-112539/ -
NLM
Ferrarezi RC. Framework para modelagem e verificação formal de programas de controle de sistemas instrumentados de segurança [Internet]. 2014 ;[citado 2024 abr. 19 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-31122015-112539/ -
Vancouver
Ferrarezi RC. Framework para modelagem e verificação formal de programas de controle de sistemas instrumentados de segurança [Internet]. 2014 ;[citado 2024 abr. 19 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-31122015-112539/
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
