27 DEZEMBRO / SEXTA FEIRA / 19:26
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

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 2024