Made available in DSpace on 2016-06-02T19:06:02Z (GMT). No. of bitstreams: 1 DissLJHC.pdf: 911507 bytes, checksum: 0af483c56c4aeb6304f9100fe71cccb9 (MD5) Previous issue date: 2004-05-27 / Financiadora de Estudos e Projetos / Generally, operating systems offer a set of services through primitives that are used on demand by applications. Similarly, software components implement and provide services through well-defined interfaces, which are reused in different software projects of a problem domain. Based upon this similarity, it is researched the reuse of software components in real time operating systems projects. It is presented CSK (Computer Structured Kernel) approach for structuring a real time kernel with software components. The approach is divided in two phases. In the first one software components are built from the legacy code and documentation of a preexisting kernel. In the second one, that kernel is rebuilt by reusing the produced components. A case study applies CSK to real time kernel Virtuoso. / Sistemas operacionais em geral oferecem um conjunto de serviços através de primitivas, as quais são utilizadas sob demanda pelas aplicações. Similarmente, componentes de software implementam e disponibilizam serviços através de interfaces bem definidas, sendo reutilizados em diferentes projetos de software de um domínio de problema. Baseado nesta similaridade, é pesquisado o reuso de componentes de software na área de tempo-real, nos projetos de sistemas operacionais. É apresentada uma abordagem para a estruturação de kernels de tempo-real utilizando componentes de software, denominada CSK (Component Structured Kernel). Esta abordagem é dividida em duas grandes fases. Na primeira fase, constroem-se os componentes a partir do código legado e da documentação de um kernel já existente. Na segunda fase é feita a reestruturação do kernel, através do reúso de componentes. Um estudo de caso aplica a abordagem CSK ao kernel Virtuoso.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.