Uso de modelos formais em sistemas pervasivos de cuidados de saúde: um estudo de caso em auxílio à prática de exercícios físicos
Uso de modelos formais em sistemas pervasivos de cuidados de saúde: um estudo de caso em auxílio à prática de exercícios físicos
<elthon@arapiraca.ufal.br>
Diversas soluções de software têm sido desenvolvidas para a área de cuidados de saúde. Nesta área, destacam-se as pesquisas em exercícios físicos, que tem recebido grande atenção da Organização Mundial de Saúde por ajudar a diminuir os riscos de diversas doenças e a aumentar a qualidade de vida das pessoas acometidas por alguma delas. Contudo, há três problemas principais nas soluções existentes desenvolvidas para o acompanhamento de exercícios físicos: i) levam em consideração apenas variáveis fisiológicas, ii) necessitam da atenção do profissional de saúde durante a prática do exercício e iii) não fornecem recomendações customizadas. Neste trabalho, é apresentado um método para proporcionar a manutenção de conformidade entre as ações dos indivíduos e as recomendações do profissional de saúde, durante a prática de exercícios, sem a presença do mesmo in loco. Tal método possibilita a construção de um modelo na forma de autômato finito. Este autômato, chamado de modelo de referência, é capaz de descrever como o indivíduo deve se comportar a fim de se manter em conformidade com as recomendações do profissional de saúde. Por ser gerado a partir da composição de modelos menores, a evolução do modelo pode ser obtida e as propriedades garantidas por construção. Além disso, propriedades de vivacidade e segurança são verificadas no modelo construído por meio da técnica de verificação de modelos, fornecendo confiabilidade ao sistema. Algumas tarefas foram executadas no processo de avaliação do método apresentado e demonstraram que: o processo de construção do modelo de referência está de acordo com o processo clínico; o modelo gerado é capaz de representar o conhecimento do especialista, fornecendo recomendações adequadas ao indivíduo; e a solução apresentada é tecnicamente viável de se implementada e executada; e,por fim,este método pode ser usado em cenários reais,desde que os indivíduos não estejam sob condições de estresse.
Several software solutions have been developed for the healthcare area. In this area, we high light the area of physical exercise that has received great attention from World Health Organization for helping decreasing risk of various diseases and improving the quality of life of people affected by some of them. However, there are three main problems with such solutions developed for monitoring of physical exercises: i) only physiological variables are supported, ii) professional attention is required during the exercise, and iii) customized recommendations are not given. In this work,we present a method to provide accordance maintenance between individuals actions and recommendations from health care professional, during the exercise execution, without the presence of himin loco. Such a method makes it possible to build a finite automaton model. Such an automaton, called reference model, describes how an individual must behave aiming to follow recommendations from the health care professional. As it is obtained by means of composition from smaller models, the model evolution is accomplished and properties are guaranteed by means of building process. Besides, liveness and safety properties are checked in the model by the model checking technique,making the model more reliable. Some tasks were performed during the evaluation process and showed that: the building process of the reference model is according to the clinical procedure; the generated reference model is able to represent the knowledge of the health care professional by providing appropriate recommendations; the presented solution is technically feasible to be developed and executed; and such a method can be used in real scenarios, since individuals are not under stress conditions.
Dr. Silva, Leandro Dias da.
Dr. Lima, Antonio Marcus Nogueira.
Dr. Pisa, Ivan Torres.
Dr. Gorgônio, Kyller Costa.
Modelos formais - Computação.
Manutenção de conformidade.
Saúde e computação.
Exercício físico - Monitoramento de praticantes.
Exercício físico e computação.
Atividade física e tecnologia.
Software - Acompanhamento de exercícios físicos.
Modelo autômato finito.
Referência
OLIVEIRA, Elthon Allex da Silva. Uso de modelos formais em sistemas pervasivos de cuidados de saúde: um estudo de caso em auxílio à prática de exercícios físicos. 2015. Tese (Doutorado em Ciência da Computação )- Programa de Pós-Graduação em Ciência da Computação, Centro de Engenharia Elétrica e Informática, Universidade Federal de Campina Grande, Campina Grande, PB, 2015