Monitoramento de propriedades em tempo real : um estudo de caso na Body Sensor Network

Abstract

A implementação de sistemas em tempo real pode ser bastante complexa no que se refere à garantia de suas propriedades em tempo de execução. Para tanto, abordagens baseadas em verificação de modelos são bastante adequadas. Nestas abordagens, primeiramente modela-se formalmente o sistema alvo utilizando ferramentas de verificação de modelos (e.g. UPPAAL), e então verificam-se as propriedades de interesse antes da implementação propriamente dita do sistema. Observa-se no entanto, que tal abordagem pode abstrair informações do sistema implementado não considerando aspectos físicos relevantes a serem considerados. Com isso, é importante que haja uma forma adequada de permitir que propriedades especificadas em verificadores de modelo sejam mapeadas adequadamente ao ambiente de implementação do sistema alvo. Para tanto, torna-se necessário o uso do conceito de monitores que observam o sistema tendo como referência as propriedades previamente verificadas e que devem ser asseguradas em tempo de execução. Neste trabalho, exercitamos este processo tendo como referência princípios de compreensão de programas, onde implementamos no Robot Operating System (ROS) monitores que observam propriedades previamente especificadas em UPPAAL. Para este trabalho, utilizou-se a Body Sensor Network (BSN), um protótipo de um sistema em tempo real implementado no ROS cujo objetivo é monitorar estados de saúde de pacientes e detectar estados de emergência por meio de uma rede sensores sem fio. Para validar a implementação, foram realizados experimentos para se obter resposta às seguintes perguntas: 1) Como monitorar propriedades de sistema na BSN em tempo real no ROS preservando sua arquitetura? 2) Dada a natureza embarcada da BSN, qual o gargalo computacional para se monitorar essas propriedades? Conclui-se mostrando que é possível realizar tal monitoramento, porém sua viabilidade depende no contexto em qual o sistema estará implementado.