Um sistema de software que apresente problemas em sua execução pode gerar conseqüências desde um simples incômodo ao usuário, até desastres como a perda de uma sonda da NASA em Marte. As atividades de teste visam identificar erros nos sistemas de software, prevenindo estas conseqüências indesejáveis. Porém, os testes podem envolver entre 30% e 40% do esforço de desenvolvimento do sistema, e em sistemas críticos, seu custo pode ser de 3 a 5 vezes maior do que o custo combinado das demais atividades. Para tentar reduzir estes custos podemos automatizar parte das atividades. No presente caso, pretende-se minimizar os casos de teste gerados manualmente, utilizando uma técnica denominada verificação de modelos. Esta técnica consiste em verificar propriedades definidas formalmente através de expressões matemáticas, utilizando uma ferramenta de verificação que simula a execução do código. Além disso, um sistema que utilize um tratamento de condições excepcionais eficiente, tem sua manutenibilidade, robustez e confiabilidade melhoradas. Por isso, definimos propriedades relacionadas ao tratamento de exceções, como ponto de entrada para a verificação de modelos. Apresentamos um ambiente de testes criado para permitir a verificação destas propriedades com o verificador Java PathFinder e a exibição das estatísticas de cobertura de testes de acordo com o critério selecionado. Este ambiente facilita a execução dos testes, pois apresenta uma interface gráfica com o usuário que permite a configuração e execução dos testes sem que seja necessária a escrita de código pelo testador. Apresentamos também o resultado do uso deste ambiente para o teste de vários programas exemplo, utilizando desde código concorrente até diferentes estratégias de tratamento de exceção e discutimos as características, cuidados no uso e limitações das ferramentas utilizadas. / A software system that shows some failure at runtime execution may bring consequences that range from a simple user annoyance to great disasters such as the lost NASA probe on Mars. The test activities aim to find errors in software systems, preventing these undesirable consequences. However, tests may take between 30% and 40% of total development time, and on critical systems, its cost can be from 3 to 5 times greater than the combined cost of the other activities. In an effort to reduce these costs, we may automate some of the activities. In this work we intend to minimize test case manual generation, using a technique called model checking. This technique involves the checking of properties defined through the use of mathematical formulas, using a tool, that simulates code execution. In addition, a system with an efficient exception handling mechanism, has its maintainability, robustness and reliability enhanced. So, in this work we define exception handling related properties, as an input for model checking. We present a test tool created to allow checking of these properties using the Java PathFinder model checker, and to list the test coverage statistics, according to the selected test criteria. This tool makes easy the test execution, since it presents a graphical user interface that allows configuration and running of tests with no need to write any lines of code. We also show the results of running several tests with the GUI, using some programs implemented with concurrent code and several exception handling techniques and discuss the main features, pitfalls and limitations of the underlying tools.

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. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Os estudos realizados no presente trabalho de tese abrangem o processo de integração de subsistemas de tempo real intensivos em software e o formalismo de geração de casos de teste. A integração de subsistemas é uma fase altamente onerosa em tempo e recursos de teste de projetos de sistemas críticos tais como plataformas de satélites. São investigados testes baseados em modelos de estado que representam a interação dos subsistemas comunicantes. O problema pesquisado é o formalismo adequado para representar requisitos de tempo no modelo comportamental da interação de modo que casos de teste possam ser derivados por métodos automáticos. Com foco na modelagem dos serviços providos pelos subsistemas em integração, propõe-se um arcabouço para teste de interoperabilidade e de robustez composto por cinco elementos estruturantes: (1) perfil do serviço, (2) modelo nominal do serviço, (3) perigos de tempo, (4) modelo aumentado do serviço, e (5) propósito de teste. O arcabouço, denominado InRob, orienta a construção de modelos formais de interoperabilidade os quais representam o comportamento de um serviço em um dado estágio de integração. Os modelos são estendidos com propriedades de tempo de modo que possam ser derivados casos de teste de robustez, relativos a desvios de tempo na troca de mensagens entre os subsistemas. A validação da abordagem InRob é feita no domínio de subsistemas espaciais, na integração dos subsistemas que compõem um instrumento imageador (telescópio) de raios X a bordo de uma missão de satélite de astronomia. Nesse estudo de caso, o InRob é instanciado em um processo de teste composto por três etapas, duas delas apoiadas por ferramentas existentes para geração e execução de casos de teste.

O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

This work presents a method to perform formal and dynamic verification of concurrent software. The objective is to provide a method capable of identifying problems in programs whose execution is based on multiple threads, and analyze behavioral properties. The method is able to detect problems in concurrent software, as well as check conformity of the concurrent software with desirable behavior, based on information collected dynamically, i.e. at runtime. The information collected consists of the software execution flow as well as data about the way communicate the software components during this run. The data collected reflect the software's execution, which ensures greater confidence to the information collected. This information is analyzed to identify deadlocks and race conditions in a process called Dynamic Analysis. In addition, this information is also used to automatically generate a model that describes the behavior of a software, which is used for verification of behavioral properties. This process is called Formal Verification. The automatic model generation eliminates the need for manual construction of the model, which requires much effort and knowledge of formal methods, this can increase costs and development time software. However, the dynamic analysis is known to only perform coverage of the current behavior of competing software systems. Current behavior is one that occurs only during an execution of concurrent software systems, without considering all other possible behaviors from the non-determinism. Due to the non-determinism, concurrent software can produce different results for the same input to each execution of software. Therefore reproduce the behavior that leads to competitive software failure is a complex task. This paper proposes a method to perform formal verification and dynamic concurrent software capable of capturing the non-deterministic behavior of these systems and provide reduced development costs by eliminating the need for manual construction of concurrent software system models. The method is validated by a case study consists of three test software systems. / Fundação de Amparo a Pesquisa do Estado de Alagoas / Neste trabalho é apresentado um método para verificação formal e dinâmica de software concorrentes. O objetivo é oferecer um método capaz de identificar problemas inerentes a programas cuja execução baseia-se em múltiplas threads, além de analisar propriedades comportamentais descritas com base nos preceitos da lógica temporal. Propõe-se um método capaz de detectar problemas e verificar formalmente a adequação da execução de sistemas de software concorrentes com relação ao comportamento desejável a tais sistemas, baseando-se em informações coletadas dinamicamente, ou seja, em tempo de execução. As informações coletadas correspondem às sequências de execução de sistemas de software, bem como dados sobre a maneira como se comunicam seus componentes durante sua execução. Os dados colhidos refletem a execução do sistema de software propriamente dito, o que garante maior confiança às informações coletadas. Tais informações são analisadas de modo a identificar impasses e condições de corrida em um processo denominado Análise Dinâmica. Ademais, estas informações também são utilizadas para geração automática de um modelo que descreve o comportamento do sistema de software, o qual é utilizado para verificação de propriedades comportamentais. A este processo de verificação dá-se o nome de Verificação Formal. A geração automática do modelo elimina a necessidade de construção manual do mesmo, que requer muito esforço e conhecimento acerca de métodos formais, isso pode aumentar custos e tempo de desenvolvimento do sistema de software. Entretanto, a análise dinâmica é conhecida por apenas realizar cobertura sobre o comportamento atual de sistemas de software concorrentes, sem considerar a análise de todas as outras possíveis sequências de execuções devido ao não determinismo. Em razão do comportamento não determinístico, sistemas de software concorrentes são capazes de produzir resultados diferentes para a mesma entrada a cada nova execução. Deste modo, reproduzir o comportamento que leva sistemas de software concorrente à falha é uma tarefa complexa. O presente trabalho propõe um método para realizar verificação formal e dinâmica de sistemas de software concorrente capaz de capturar o comportamento não determinístico desses sistemas, além de proporcionar a redução de custos de desenvolvimento através da eliminação da necessidade de construção manual de modelos de sistemas de software concorrente. O método é validado através de um estudo de caso composto por testes em três sistemas de software.

O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

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. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T13:51:53Z No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:49:26Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:52:49Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Made available in DSpace on 2015-07-23T15:52:49Z (GMT). No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) Previous issue date: 2013-12-20 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, computational systems specialized to do a function in larger systems, electronic or mechanical, is growing in the daily life, and it is becoming increasingly important to ensure the robustness of these systems. There are several techniques to ensure that a system is released without error. In particular, formal verification is proving very effective in finding bugs in programs. In this work, we describe the formal verification for C++ Programs and correctness proof by mathematical induction. Both techniques will be developed using the tool Efficient SMT-Based Context-Bounded Model Checker (ESBMC), a model checker based on satisfiability modulo theories and first order logic. The experiments show that the tool can be used to check a wide range of applications, from simple test cases to commercial applications. The tool also proved to be more efficient than other models checkers to verify C++ programs, finding a greater number of bugs, and supporting a larger number of the features that the language C++ has to offer, in addition to being able to prove several properties, using the method of mathematical induction. / A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.

A UML (Unified Modeling Language) é uma linguagem de modelagem para especificar, construir e documentar artefatos de sistemas de software. A UML-RT, usada pela ferramenta Rational Rose RealTime (RoseRT), é uma extensão da UML que permite a modelagem de sistemas de tempo real distribuídos e guiados por evento. A UML-RT não possui semântica formal, logo não é possível realizar verificação formal do modelo. O presente trabalho propõe o mapeamento dos elementos de comunicação da UML-RT para a álgebra de processos p-calculus, a fim de prover semântica formal à UML-RT. Com objetivo de automatizar o mapeamento, foi desenvolvido um protótipo de tradutor que captura o modelo UML-RT especificado na ferramenta RoseRT e determina suas definições p-calculus. As definições p-calculus geradas utilizam a sintaxe da gramática do HAL-JACK, que é uma ferramenta integrada para verificação e análise de sistemas expressos em p-calculus, assim as definições p-calculus podem ser submetidas ao HAL-JACK para verificação formal de propriedades. Este trabalho detalha o mapeamento UML-RT para p-calculus, descreve o protótipo desenvolvido e apresenta alguns exemplos do mapeamento do modelo UML-RT para definições p-calculus.

Entre as principais dificuldades do desenvolvimento de software embarcado crítico e de tempo real está a especificação e o processo de verificação e validação apoiado ao projeto conceitual. Neste contexto, a modelagem de sistemas tem uma importante função, uma vez que um processo complexo possa ser analisado e validado antes de sua real implementação. Esta dissertação aborda o problema de verificação e validação de software embarcado de um satélite com configuração ACDH (Attitude Control and Data Handling) através de uma plataforma aerosuspensa com um grau de liberdade, utilizando a SysML, a ferramenta CASE TELELOGIC Rhapsody e a orientação das normas da ECSS (European Cooperation on Space Standardization). A partir do modelo obtido, são utilizadas três abordagens para análise e avaliação: (1) Especificação e gerenciamento dos requisitos, através dos conceitos determinados pela ECSS; (2) Modelagem do sistema e verificação dos requisitos, através do formalismo matemático dos autômatos utilizando a técnica de model checking através da ferramenta UPPAL; (3) Conversão do modelo em SysML, aplicando a Engenharia de Requisitos e o processo de verificação e validação do sistema, através da simulação na ferramenta CASE.