A tool for automatic model extraction of Ada/SPARK programs
This 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 model checker to verify timing properties is discussed.
|2010||A tool for automatic model extraction of Ada/SPARK programs||André Carvalho; Nuno Silva; Simão Melo de Sousa; Nelma Moreira||Capítulo ou Parte de Relatório|