|
|
||||||||
|
|||||||||
|
Technical Report: DCC-2011-02A Tool for Automatic Model Extraction of Ada/SPARK Programs (Part II)Sabine Broda, Nelma MoreiraCMUP & DCC-FC, Universidade do Portoe-mail: {sbb,nam}@dcc.fc.up.pt Nuno SilvaDCC-FC & LIACC, Universidade do Porto , PortugalE-mail: nunomiguel06@gmail.com Simão Melo de SousaDepartamento de Informática, Universidade da Beira Interior & LIACC, PortugalE-mail: desousa@di.ubi.pt October 2011 AbstractThis 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. |
||||||||
|