Please use this identifier to cite or link to this item: http://hdl.handle.net/1843/RVMR-82UHY3
Type: Tese de Doutorado
Title: Modelagem, verificação formal e codificação de sistemas reativos autônomos
Authors: Ruiter Braga Caldas
First Advisor: Sergio Vale Aguiar Campos
First Co-advisor: Raimundo da Silva Barreto
First Referee: Antonio Alfredo Ferreira Loureiro
Second Referee: Antonio Otavio Fernandes
Third Referee: Linnyer Beatrys Ruiz
metadata.dc.contributor.referee4: Djamel F.h. Sadok
Abstract: Os sistemas computacionais são utilizados nas mais variadas áreas da vida cotidiana, desde o controle das contas bancárias até os pacientes nos hospitais. Nas aplicações onde vidas humanas ou altos investimentos estão em risco, a qualidade dos sistemas computacionais tem uma importância fundamental para eliminar ou reduzir as falhas. A utilização de modelos formais no processo de desenvolvimento de sistemas apresentam uma resposta ao problema citado, pois oferecem uma descrição das partes mais relevantes do sistema com um nível adequado de abstração. Este trabalho apresenta o Modelo de Desenvolvimento Bare, para o desenvolvimento de aplicações em Sistemas Reativos Autônomos e mostra a possibilidade de modelar aplicações para diversas área. O modelo inicia com a descrição da aplicação por meio de uma máquina de estados finito, chamada X-machine. A aplicação a ser desenvolvida é a peça principal, ou núcleo, de um sistema reativo onde os eventos detectados no ambiente são capturados, avaliados com base no estado corrente da máquina, produzindo como resposta ao evento uma transição de estado e um elemento de atuação, que pode ser um novo evento ou uma comunicação. No Modelo Bare a especificação da aplicação é feita usando uma ferramenta gráfica chamada GeradorXM, após a modelagem da aplicação a X-machine resultante é transformada para um modelo tabular, onde cada linha é independente e contém informação suficiente para executar uma computação. A aplicação no modelo tabular é carregada na plataforma alvo, onde é interpretada por um programa pequeno, chamado ExecutorXM, que é o responsável pela execução da aplicação. Antes de executar a aplicação um modelo do sistema é gerado pelo GeradorXM para ser utilizado como entrada para a ferramenta de verificação de modelos NuSMV. Com isso as propriedades desejáveis para a aplicação podem ser verificadas para confirmar a sua correção. A execução do modelo Bare fecha um ciclo de desenvolvimento de aplicação para sistemas reativos autônomos por meio de um modelo formal, com geração automática de código para um interpretador e verificação de propriedades para o modelo do sistema.
Abstract: The computation systems are used in many areas, since bank account´s until patient's monitoring. Applications where human lives and high investments are critical, the system´s quality is fundamental to reduces or eliminate failures. The formal methods are used to describe parts of the system using appropriate level of abstraction. This thesis presents the Bare Model to development of applications in Autonomous Reactive System´s and shows his capabilities to development many applications. The model starts with a application description by a finite state machine, called X-machine. The application acts as a centerpiece, or core, of a reactive system. The events detected in the environment are captured and evaluated, based on the current state of the machine. The response to the events detected are the transitions of states and the actions, which can be an new event or just a communication. On the Bare Model, the specification of the application is done by using a graphical tool called GeradorXM. After the design, the X-machine is transformed to a tabular model, where each line is independent and contains enough information to perform a computation. The tabular model is uploaded into the target hardware, where it is interpreted by a small code, called ExecutorXM, which is responsible for his execution. Before to run the application, a model of the system can be generated to be used as an input to the NuSMV, which is a model checking's tool. Thus the desirable properties for the application may be checked to confirm its correctness. Thus closing a cycle of applications development to autonomou´s reactive systems using a formal model, with automatic code generation which is executed by an translator and using formal verification of properties for the system model.
Subject: Software de aplicação Desenvolvimento
Computação
language: Português
Publisher: Universidade Federal de Minas Gerais
Publisher Initials: UFMG
Rights: Acesso Aberto
URI: http://hdl.handle.net/1843/RVMR-82UHY3
Issue Date: 17-Dec-2009
Appears in Collections:Teses de Doutorado

Files in This Item:
File Description SizeFormat 
teseruiter.pdf9.84 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.