A tool for automatic model extraction of Ada/SPARK programs

This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool th...

ver descrição completa

Detalhes bibliográficos
Autor principal: André Carvalho (author)
Outros Autores: Nuno Silva (author), Simão Melo de Sousa (author), Nelma Moreira (author)
Formato: other
Idioma:eng
Publicado em: 2010
Assuntos:
Ciência de computadores, Ciências da computação e da informação
Computer science, Computer and information sciences
Texto completo:https://hdl.handle.net/10216/53339
País:Portugal
Oai:oai:repositorio-aberto.up.pt:10216/53339
Descrição
Resumo:This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool that automatically generates models (timed automata) from Ada/RavenSPARK source code and uses the model checker to verify timing properties is discussed.

Registros relacionados