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.