Ferramenta para Auxiliar o Processo de Verificação Formal de Propriedades em Programas AADL
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
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.
