Departamento de Inform\'atica / CCTC
Universidade do Minho, Braga, Portugal
E-mail: andre.t3nsion@gmail.com
DCC-FC & LIACC, Universidade do Porto , Portugal
E-mail: nunomiguel06@gmail.com
Departamento de Informática, Universidade da Beira Interior & LIACC, Portugal
E-mail: desousa@di.ubi.pt
DCC-FC & LIACC, Universidade do Porto
E-mail: nam@ncc.up.pt}
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.