A tool for automatic model extraction of Ada/SPARK programs

• Type: Chapter or Part of a Report
• Date: 2010

Authors

André Carvalho (Author) Other; Nuno Silva (Author) Other; Simão Melo de Sousa (Author) FCUP; Nelma Moreira (Author) FCUP

Scientific classification

FOS: Natural sciences > Computer and information sciences

CORDIS: Physical sciences > Computer science

Other information

Abstract (EN): 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.

Language: English

Type (Professor's evaluation): Scientific

Notes: Technical Report DCC-2010-05, DCC - FC, Universidade do Porto, August, 2010.