Ferramenta para Auxiliar o Processo de Verificação Formal de Propriedades em Programas AADL

  • Rafael de Oliveira
  • Gabriel Santos UFSC
  • Jean-Marie Farines UFSC
  • Leandro Becker UFSC

Resumo


A especificação de propriedades para a realização de verificação formal de sistemas não é uma tarefa trivial. Normalmente esse tipo de atividade requer uma grande experiência por parte do projetista, necessitando a utilização de uma linguagem própria, como por exemplo a lógica temporal. Apesar desta linguagem ser poderosa, estas propriedades não refletem de forma direta o modelo do sistema. Este trabalho visa suprir esta dificuldade propondo um assistente para especificação de propriedades de verificação o qual faz uso de linguagem natural ao usuário. O assistente proposto apresenta as propriedades utilizando padrões pré-definidos, que são posteriormente traduzidos para lógica temporal. Além deste assistente, neste trabalho é desenvolvida uma forma de visualizar os resultados de verificação, permitindo a simulação do modelo do sistema. Para validar as ferramentas desenvolvidas realizou-se um estudo de caso, o qual consistiu da especificação e verificação de propriedades de um sistema de marcapasso. O presente trabalho se enquadra no escopo do projeto Topcased, o qual se baseia fortemente na linguagem de modelagem AADL.

Referências

R. G. Oliveira "Contribuies para Melhoria do Processo de Verificao Formal de Propriedades em Programas AADL." Dissertao de Mestrado. Universidade Federal de Santa Catarina (UFSC) 2011.

G. H. R. Santos "Modelagem e Verificao Formal de Softwares com AADL: Contribuies e Estudo de Caso " Relatrio de estgio. Universidade Federal de Santa Catarina 2011.

Topcased "Toolkit in OPen-source for Critical Applications and SystEms Development. URL http://www.topcased.org " 2011. [Online]. Available: http://www.topcased.org

P. Feiler D. Gluch and J. Hudak "The Architecture Analysis & Design Language (AADL): An introduction " Software Engineering Institute Carnegie Mellon University Tech. Rep. 2006.

B. R. Larson "Behavior Language for Embedded Systems with Software Annex Sublanguage for AADL. Draft Version v0.13 " 2010.

M. Bozzano A. Cimatti J.-P. Katoen V. Y. Nguyen T. Noll and M. Roveri "The compass approach: Correctness modelling and performability of aerospace systems " in Proceedings of the 28th International Conference on Computer Safety Reliability and Security ser. SAFECOMP '09. Berlin Heidelberg: Springer-Verlag 2009 pp. 173-186.

L. B. Becker J. Farines J. Bodeveix M. Filali and F. Vernadat "Development process for critical embedded systems " Architecture pp. 95-108 2010.

B. Berthomieu P. O. Ribet and F. Vernadat "The tool tina - construction of abstract state spaces for petri nets and time petri nets " International Journal of Production Research 2004.

M. Dwyer G. S. Avrunin and J. C. Corbett "Patterns in property specifications for finite-state verification " In Proceedings of the 21st International Conference on Software Engineering May 1999.

B. Brard et. al. Systems and Software Verification - Model Checking Techniques and Tools. Editora Springer. 1999.

A. P. Sistla "Safety liveness and fairness in temporal logic " Formal Aspects of Computing vol. 6 no. 5 pp. 495-511 1994. [Online]. Available: http://www.springerlink.com/index/10.1007/BF01211865

BostonScientific "Pacemaker system specification " Tech. Rep. January 2007.
Publicado
07/11/2011
DE OLIVEIRA, Rafael; SANTOS, Gabriel; FARINES, Jean-Marie; BECKER, Leandro. Ferramenta para Auxiliar o Processo de Verificação Formal de Propriedades em Programas AADL. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SISTEMAS COMPUTACIONAIS (SBESC), 1. , 2011, Florianópolis. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2011 . p. 27-32. ISSN 2237-5430.