16 APRIL / WEDNESDAY / 04:29
FCUP PT 
 EN
 
 
INFORMATION
STAFF
EDUCATION
RESEARCH
LIBRARY
NEWS
CONTACTS

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
E-mail: andre.t3nsion@gmail.com

Nuno Silva

DCC-FC & LIACC, Universidade do Porto , Portugal
E-mail: nunomiguel06@gmail.com

Sim�o Melo de Sousa

Departamento de Inform�tica, Universidade da Beira Interior & LIACC, Portugal
E-mail: desousa@di.ubi.pt

Nelma Moreira

DCC-FC & LIACC, Universidade do Porto
E-mail: nam@ncc.up.pt}

Rua do Campo Alegre, 4169-007 Porto, Portugal

August 2010

Abstract


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.

FCUP 2025