A tool for automatic model extraction of Ada/SPARK programs

• Tipo: Capítulo ou Parte de Relatório
• Data: 2010

Autores

André Carvalho (Autor) Outra; Nuno Silva (Autor) Outra; Simão Melo de Sousa (Autor) FCUP; Nelma Moreira (Autor) FCUP

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

CORDIS: Ciências Físicas > Ciência de computadores

Outras Informações

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Notas: Technical Report DCC-2010-05, DCC - FC, Universidade do Porto, August, 2010.