Technical Report: DCC-2010-05

A Tool for Automatic Model Extraction of Ada/SPARK Programs

André Carvalho

Departamento de Inform\'atica / CCTC
Universidade do Minho, Braga, Portugal

Nuno Silva

DCC-FC & LIACC, Universidade do Porto , Portugal

Simão Melo de Sousa

Departamento de Informática, Universidade da Beira Interior & LIACC, Portugal

Nelma Moreira

DCC-FC & LIACC, Universidade do Porto

Rua do Campo Alegre, 4169-007 Porto, Portugal

August 2010


his 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 \upp model checker to verify timing properties is discussed.