Modelagem, verificação formal e codificação de sistemas reativos autônomos

AUTOR(ES)
FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

17/12/2009

RESUMO

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.

ASSUNTO(S)

computação teses. software de aplicação desenvolvimento.

ACESSO AO ARTIGO

Documentos Relacionados