Técnicas de modelagem formal aplicadas na avaliação de sistemas biomédicos

Técnicas de modelagem formal aplicadas na avaliação de sistemas biomédicos.

Misael Costa Júnior

Disciplina (SSC5793): Especificação Formal de Software

Prof. Dr. Adenilso Simão

2

Roteiro

Contextualização Artigo

Conclusões e futuras tendências Referências

Roteiro


1. Contextualização Teste de software Teste vs Métodos Formais Usage Model Sistemas biomédicos Tendências

2. Artigo Autores Objetivos Metodologia Resultados e discussão Questionamentos ao autor

3. Conclusões e futuras tendências

4. Referências

•  Objetivo: revelar a presença de defeitos; •  Um conjunto de atividades que pode ser planejada antecipadamente e

realizada de forma sistemática;

•  Atividades realizadas ao longo do desenvolvimento, que verificam se o software e seus componentes atendem às especificações;

3

Teste de software


Roteiro



TestesdeSo)waregarantemqueosistemafoidesenvolvidocorretamenteeomesmopossuiascaracterís9casdequalidadeesperadas.

Teste de software Teste vs Métodos Formais Usage Model Sistemas biomédicos Tendências

•  Alguns sistemas exigem testes mais confiáveis; •  Aplicação de validação com maior nível de rigor; •  Teste + base matemática; •  Teste formal:

•  Geração de casos de testes através da especificação formal; •  Inserir especificações formais para utilizarmos testes; •  Adotar especificações formais utilizadas em outras técnicas de verificação formal que

estejam sendo aplicadas.

•  Classificações: •  Orientados a modelos; •  Orientados a propriedades; •  Orientados a comportamento; •  Híbridos.

4

Teste vs Métodos Formais


Roteiro




•  Alguns sistemas exigem testes mais confiáveis; •  Aplicação de validação com maior nível de rigor; •  Teste + base matemática; •  Teste formal:

•  Geração de casos de testes através da especificação formal; •  Inserir especificações formais para utilizarmos testes; •  Adotar especificações formais utilizadas em outras técnicas de verificação formal que

estejam sendo aplicadas.

•  Classificações: •  Orientados a modelos; •  Orientados a propriedades; •  Orientados a comportamento; •  Híbridos.

5

Teste vs Métodos Formais


Roteiro




•  Representação formal de software de um dispositivo em particular;

•  Mecanismo de documentação; •  Iteração entre usuário e sistema; •  Agências reguladoras visam assegurar

condições mínimas de segurança; •  A estrutura de um “usage model”

contém três camadas: •  Dados de suporte; •  Visão geral; •  Detalhes de uso.

6

Usage Models


Roteiro




7

Usage Models


Roteiro



Visãogeraldaestruturadeum“usagemodel”.


8

Sistemas biomédicos


Roteiro



•  Sistemas que apoiam a decisão clinica; •  Dentre esses sistemas, destacam-se:

•  Sistemas de diagnóstico de ultra-sonografia; •  Sistemas de processamento de linguagem; •  Sistemas de gerenciamento de informações

hospitalares; •  Sistemas de diagnóstico radiológico.

•  Necessidade de verificação e validação; •  Agências reguladoras (Exemplo: FDA).


9

Sistemas biomédicos


Roteiro



•  Sistemas que apoiam a decisão clinica; •  Dentre esses sistemas, destacam-se:

•  Sistemas de diagnóstico de ultra-sonografia; •  Sistemas de processamento de linguagem; •  Sistemas de gerenciamento de informações

hospitalares; •  Sistemas de diagnóstico radiológico.

•  Necessidade de verificação e validação; •  Agências reguladoras (Exemplo: FDA).


10

Objetivos


Roteiro



•  Identificar métodos, estratégias e abordagens de teste de software e/ou análise de qualidade em sistemas biomédicos;

•  Obter um visão geral dos principais procedimentos experimentais adequados para validar sistemas biomédicos; •  Catalogar as principais limitações e dificuldades em análises de sistemas

biomédicos.


11

Resultados


Roteiro



Relação entre abordagens

Métodos formais

Outras abordagens.


12

Discussão


Roteiro



•  Dificuldade em manter a integridade e qualidade do software; •  Falta de arquiteturas padrão; •  Agências reguladoras ainda não adotam integralmente teste baseados em

métodos formais;

•  Alguns autores enfatizam a necessidade de testes mais rigorosos.


13

Artigo


•  Titulo: A Formal Methods Approach to Medical

Device Review;

•  Autores: Raoul Jetley, Purushotaman Iyer and Paul L. Jones;

•  Ano: 2006;

•  Veículo de publicação: IEEE Xplorer Digital Library;

•  Origem: Colaboração entre academia e indústria;

•  Citações: 59.

Roteiro



Autores Objetivos Metodologia Resultados e discussão Questionamentos ao autor

14

Autores


Roteiro




RaoulJetley15anosdeexperiênciaemregulamentação,indústriaenaacademia.NorthCarolinaStateUniversityDoctorofPhilosophy(Phd.),ComputerScience2004–2006NorthCarolinaStateUniversityMaster’sDegree,ComputerScience2000–2002UniversityofMumbaiBachelor’sDegree,ComputerScience1994–1998

hQps://www.linkedin.com/in/raoul-jetley-0302641

15

Objetivos


Roteiro




•  Aplicação de técnicas e métodos formais visando avaliar o software de dispositivos médicos;

•  Desenvolvimento de modelos de uso para auxiliar na avaliação pré-mercado; •  Utilização de técnicas “slicing” orientadas à abstração na avaliação pós-

mercado;

•  Avaliação para regulamentação de dispositivos médicos; •  Avaliação de projeto (pré-mercado); •  Desempenho do produto (vigilância pós-mercado).

•  Desenvolvimento de modelos de uso (bombas de infusão); •  Avaliação pré-mercado (modelos de uso); •  Avaliação pós-mercado (técnicas orientadas a corte); •  Abstração para facilitar a análise forense pós-mercado; •  Definição do modelo com base em técnicas de especificação baseadas em

métodos formais.

16

Metodologia


Roteiro




17

Metodologia


Roteiro




Esquema de modelo da CDRH’s para análise pré-mercado.

Estudo de caso – Modelo de uso de uma bomba de infusão

18

Metodologia


Roteiro




19

Metodologia


Roteiro




Bombadeinfusão.

•  BombadePerfusão;•  Disposi9vomédicodesegurançacri9ca;•  So)ware+Hardware;•  U9lizadoparaperfundirlíquidos;•  Categorizadaspelosautoresem:

•  Grandevolume;•  Analgesiacontroladapelopaciente(PCA);•  Elastométricas;•  Implantadas;•  Ambulatoriais.

20

Metodologia


Roteiro




ModelodeusodosoLwaredabombadeinfusão.

•  Núcleomodeladocomoumautômatofinito;•  Astransiçõesrepresentaminsumosfornecidos

porumusuáriohumano;•  Nototal,omodeloconsistede292estadose

3.500transições;•  Omodelofoiu9lizadoparatestarumprotó9po

doso)waredabombadeinfusão(PCA)desenvolvidanoOSEL;

•  39milsequênciasdecasosdetestesforamderivadas;

•  44errosforamrelavadosatravésdostestesrealizados,dosquais5eramerrosgraves.

Análise forense pós-mercado – Program Slicing

21

Metodologia


Roteiro




•  +Análise pré-mercado - Análise pós-mercado; •  Código analisado manualmente; •  Program Slicing; •  Com base nos cortes produzidos, uma parte do programa é identificada para

auxiliar na busca dos erros.

22

Metodologia


Roteiro




23

Artigo


•  Titulo: Program Slicing

•  Autores: Mark Weiser

•  Ano: 1981

•  Veículo de publicação: ACM Digital Library

•  Origem: Academia

•  Citações: 3.832

Roteiro




24

Program Slicing


Roteiro




•  Programa de cortes ou fatias; •  Método usado para abstrair códigos-fonte; •  A partir de um subconjunto de um programa, o corte reduz esse programa

para um tamanho mínimo;

•  O corte (programa reduzido) é uma representação do programa original; •  Um algoritmo de fluxo de dados busca o corte.

25

Program Slicing


Roteiro




Abordagem integrada

26

Metodologia


Roteiro




•  A análise baseada em cortes nem sempre é eficiente, principalmente em programas de grande porte;

•  As abstrações de código acabam sendo muito grandes; •  Combinação do corte estático com o modelo de abstração; •  Diminuir o número de iterações necessárias e de cortes durante a análise.

27

Metodologia


Roteiro




28

Metodologia


Roteiro




Algoritmoquedescreveaabordagemintegradaparaaanáliseforense,combinandooprogramaslicingcomaabstração.

Estudo de caso: Xio System

29

Metodologia


Roteiro




30

Metodologia


•  O módulo consistiu de 40.000 linhas de código em

C;

•  Para analise os autores realizaram: •  Corte estático único para rastrear erros; •  Combinação entre o modelo de abstração com o código;

•  Ambas as abordagens traçaram erros com sucesso;

•  A abordagem integrada necessitou de 39% de menos esforço.

Roteiro




ImagemdoXioSystem.

31

Metodologia


Roteiro




Umaabordagembaseadaemcorteparaavaliaçãopós-mercado

32

Metodologia


Roteiro




AnáliseforensedoXioSystem:corteestáYcovsabordagemintegrada.

33

Resultados e discussão


Roteiro




•  As duas abordagens apresentadas no estudo, pré-comercialização e pós-comercialização, foram eficazes;

•  Mesmo com o sucesso das abordagens, há pouca aceitação da FDA e dos fabricantes de dispositivos médicos; •  Estudos em larga escala evidenciam as vantagens em se usar ferramentas

baseadas em métodos formais.

34

Questionamentos ao autor


Roteiro




1.  O estudo claramente afirma que o modelo apresentado foi utilizado em protótipos. Dessa forma, existe algum trabalho em que descreva o uso do modelo em um dispositivo real?

R. O modelo não foi usado diretamente para verificar os dispositivos do mundo real. Em vez disso, nós o utilizamos para verificar modelos de simulação de dispositivos médicos. Uma vez verificado, estes modelos de simulação podem ser usados como uma base para os dispositivos reais.

2.  Desde o período de publicação, a FDA ou empresas de desenvolvimento de dispositivos médicos já utilizaram o modelo em algum produto no mercado?

R. Nós não temos qualquer dispositivo no mercado. Este trabalho foi parte de um projeto de pesquisa financiado pelo FDA dos EUA, e não envolveu qualquer fabricante de dispositivo. As abordagens de modelos formais desenvolvida foram publicadas em domínio público e qualquer fabricante que queira usá-las é livre para isso.

3.  As abordagens descritas no trabalho foram aplicadas em outros dispositivos? R. Nós aplicamos esta abordagem a vários tipos de bombas de infusão. Isso inclui principalmente bombas de insulina e bombas de Analgesia Controlada pelo Paciente (PCA).

35

Questionamentos ao autor


Roteiro




RepositórioOnline

•  Em geral, a avaliação de sistemas críticos é algo difícil de se realizar; •  Não há arquiteturas padrão para auxiliar nessas atividades;

•  O incentivo entre indústria e academia ainda é mínimo;

•  A literatura mostra que o desenvolvimento de métodos formais vêm crescendo.

36

Conclusões e futuras tendências


Roteiro



•  [1] Jetley, Raoul, S. Purushothaman Iyer, and Paul L. Jones. "A formal methods approach to medical device review." Computer 39.4 (2006): 61-67. •  [2] Weiser, Mark. "Program slicing." Proceedings of the 5th international

conference on Software engineering. IEEE Press, 1981. •  [3] J. Rushby, Formal Methods and the Certification of Critical Systems, tech.

report, Computer Science Laboratory, SRI Int’l, Dec. 1993. •  [4] Offutt, A. J. Investigations of the software testing coupling effect. ACM

Transactions on Software Engineering and Methodology, v. 1, n. 1, p. 5–20, 1992. •  [5] Offutt, A. J. Investigations of the software testing coupling effect. ACM

Transactions on Software Engineering and Methodology, v. 1, n. 1, p. 5–20, 1992. •  [6] Myers, G.; Sandler, C.; Badgett, T.; Thomas, T. The art of software testing.

Business Data Processing: A Wiley Series. Wiley, 2004. •  [7] Delamaro, M.; Maldonado, J.; Jino, M. Introdução ao teste de software. 1°

ed. São Paulo, SP: Elsevier, 2007.

37

Referências


Roteiro




Misael Costa Júnior [email protected]

Prof. Dr. Adenilso Simão

[email protected]