Technical Report: DCC-2011-02

A Tool for Automatic Model Extraction of Ada/SPARK Programs (Part II)

Sabine Broda, Nelma Moreira

CMUP & DCC-FC, Universidade do Porto
e-mail: {sbb,nam}

Nuno Silva

DCC-FC & LIACC, Universidade do Porto , Portugal

Simão Melo de Sousa

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

October 2011


This paper presents a brief description of the current work on a tool that analyses temporal behavior of Ada/RavenSPARK programs and, with the use of a translation algorithm, outputs an Uppaal system that simulates the program?s control flow. The focus will be the translation algorithm, it?s implementation and syntactic scope, along with results and difficulties encountered during the development process.